Struct rust_examples::dependent::Succ

pub struct Succ<N: Nat>(_);

Type-level definition of a successor of a natural number N, i.e. the number N + 1.

Trait Implementations

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

fn lower() -> usize

Lower N from a type-level to a term-level value.

impl<M, N, X> AddEq<N, Succ<X>> for Succ<M> where
    M: Nat + AddEq<N, X>,
    N: Nat,
    X: Nat, 

Addition is associative: ![N]: (M + 1) + N = (X + 1) if X = M + N => M: AddEq<N, X>

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

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