Struct rust_examples::dependent::Zero

pub struct Zero;

Type-level definition of the natural number 0.

Trait Implementations

impl HList<Zero> for HNil

HNil is an empty HList (i.e. of length N = 0).

fn cons<H>(self, x: H) -> HCons<Succ<N>, N, H, Self> where
    Self: Sized, 

Add given element to the front of this HList.

fn conctat<M, L, X, R>(self, _hlist: L) -> R where
    Self: Sized,
    M: Nat + AddEq<N, X>,
    L: HList<M>,
    X: Nat,
    R: HList<X>, 

Concatenate this and given HList.

fn len(&self) -> usize

Analogy to Vec::len.

impl Nat for Zero

fn lower() -> usize

Lower Zero from type to the term 0.

impl<N: Nat> AddEq<N, N> for Zero

Zero is the neutral element of addition: ![N]: 0 + N = X = N

impl Pred<Zero> for Zero

Zero is a predecessor of Zero.