22 val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
24 val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
26 val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
28 val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
30 val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
32 val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1
34 val compare_inv_rect_Type4 :
35 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
37 val compare_inv_rect_Type3 :
38 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
40 val compare_inv_rect_Type2 :
41 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
43 val compare_inv_rect_Type1 :
44 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
46 val compare_inv_rect_Type0 :
47 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
49 val compare_discr : compare -> compare -> __
51 val compare_invert : compare -> compare
59 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
62 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
65 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
68 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
71 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1
73 val pos_inv_rect_Type4 :
74 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
75 'a1) -> __ -> 'a1) -> 'a1
77 val pos_inv_rect_Type3 :
78 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
79 'a1) -> __ -> 'a1) -> 'a1
81 val pos_inv_rect_Type2 :
82 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
83 'a1) -> __ -> 'a1) -> 'a1
85 val pos_inv_rect_Type1 :
86 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
87 'a1) -> __ -> 'a1) -> 'a1
89 val pos_inv_rect_Type0 :
90 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
91 'a1) -> __ -> 'a1) -> 'a1
93 val pos_discr : pos -> pos -> __
99 val nat_of_pos : pos -> Nat.nat
101 val succ_pos_of_nat : Nat.nat -> pos
103 val plus : pos -> pos -> pos
105 val times : pos -> pos -> pos
112 val minusresult_rect_Type4 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
114 val minusresult_rect_Type5 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
116 val minusresult_rect_Type3 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
118 val minusresult_rect_Type2 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
120 val minusresult_rect_Type1 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
122 val minusresult_rect_Type0 : 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1
124 val minusresult_inv_rect_Type4 :
125 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
127 val minusresult_inv_rect_Type3 :
128 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
130 val minusresult_inv_rect_Type2 :
131 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
133 val minusresult_inv_rect_Type1 :
134 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
136 val minusresult_inv_rect_Type0 :
137 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1
139 val minusresult_discr : minusresult -> minusresult -> __
141 val partial_minus : pos -> pos -> minusresult
143 val minus : pos -> pos -> pos
145 val eqb : pos -> pos -> Bool.bool
147 val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
149 val leb : pos -> pos -> Bool.bool
151 val pos_compare : pos -> pos -> compare
153 val two_power_nat : Nat.nat -> pos
155 val two_power_pos : pos -> pos
157 val max : pos -> pos -> pos