Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleType
From a type znz representing a cyclic structure Z/nZ,
we produce a representation of Z/2nZ by pairs of elements of znz
(plus a special case for zero). High half of the new number comes
first.
From a cyclic representation w, we iterate the zn2z construct
n times, gaining the type of binary trees of depth at most n,
whose leafs are either W0 (if depth < n) or elements of w
(if depth = n).
Fixpoint word (
w:
Type) (
n:
nat) :
Type :=
match n with
|
O =>
w
|
S n =>
zn2z (
word w n)
end.