Trait rust_examples::dependent::AddEq

pub trait AddEq<N, X> { }

Relation M: AddEq<N, X> is interpreted as M + N = X.

An obvious alternative is to define trait EqAdd<M, N> {} with the interpretaton:

Relation X: EqAdd<M, N> is interpreted as X = M + N.

The problem with such an approach is in the specification of Zero being the neutral element:

impl<N: Nat> EqAdd<Zero, N> for N {}

Since N here is generic, it would need Specialization for it not to overlap with the specification of associativity:

impl<M: Nat, N: Nat, X: Nat + EqAdd<M, N>> EqAdd<M, Succ<N>> for Succ<X> {}

Implementors

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> AddEq<N, N> for Zero

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