Library Coq.Numbers.Cyclic.Abstract.CarryType


Set Implicit Arguments.

#[universes(template)]
Variant carry (A : Type) :=
| C0 : A -> carry A
| C1 : A -> carry A.