22 (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
26 Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> (Nat.nat
31 (* singleton inductive, whose constructor was mk_Aop *)
34 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
37 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
40 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
43 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
46 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
49 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
51 val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
53 val aop_inv_rect_Type4 :
54 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
57 val aop_inv_rect_Type3 :
58 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
61 val aop_inv_rect_Type2 :
62 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
65 val aop_inv_rect_Type1 :
66 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
69 val aop_inv_rect_Type0 :
70 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
73 val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
75 val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
79 (* singleton inductive, whose constructor was mk_ACop *)
81 val aCop_rect_Type4 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
83 val aCop_rect_Type5 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
85 val aCop_rect_Type3 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
87 val aCop_rect_Type2 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
89 val aCop_rect_Type1 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
91 val aCop_rect_Type0 : 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2
93 val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop
95 val aCop_inv_rect_Type4 :
96 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
98 val aCop_inv_rect_Type3 :
99 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
101 val aCop_inv_rect_Type2 :
102 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
104 val aCop_inv_rect_Type1 :
105 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
107 val aCop_inv_rect_Type0 :
108 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2
110 val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __
112 val dpi1__o__aop__o__op :
113 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
115 val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1
117 val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop
119 type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
120 filter : (Nat.nat -> Bool.bool) }
122 val range_rect_Type4 :
123 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
126 val range_rect_Type5 :
127 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
130 val range_rect_Type3 :
131 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
134 val range_rect_Type2 :
135 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
138 val range_rect_Type1 :
139 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
142 val range_rect_Type0 :
143 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1 range
146 val enum : 'a1 range -> Nat.nat -> 'a1
148 val upto : 'a1 range -> Nat.nat
150 val filter : 'a1 range -> Nat.nat -> Bool.bool
152 val range_inv_rect_Type4 :
153 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
156 val range_inv_rect_Type3 :
157 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
160 val range_inv_rect_Type2 :
161 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
164 val range_inv_rect_Type1 :
165 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
168 val range_inv_rect_Type0 :
169 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
172 val range_discr : 'a1 range -> 'a1 range -> __
174 type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }
177 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
181 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
185 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
189 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
193 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
197 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
200 val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop
202 val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1
204 val dop_inv_rect_Type4 :
205 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
208 val dop_inv_rect_Type3 :
209 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
212 val dop_inv_rect_Type2 :
213 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
216 val dop_inv_rect_Type1 :
217 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
220 val dop_inv_rect_Type0 :
221 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
224 val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __