Trait rust_examples::dependent::Pred

pub trait Pred<N> { }

Trait encoding a predecessor relation: “Self is a predecessor of N”.

Implementors

impl Pred<Zero> for Zero

Zero is a predecessor of Zero.

impl<N: Nat> Pred<Succ<N>> for N

For each Succ<N: Nat> = N + 1 there is a predecessor N: Nat.