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.
Inductive zn2z :=
|
W0 :
zn2z
|
WW :
znz ->
znz ->
zn2z.
Definition zn2z_to_Z (
wB:Z) (
w_to_Z:znz->Z) (
x:zn2
z) :=
match x with
|
W0 => 0
|
WW xh xl =>
w_to_Z xh *
wB +
w_to_Z xl
end.
End Zn2Z.
Implicit Arguments W0 [
znz].
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.