source: driver/extracted/util.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 6.4 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Jmeq
22
23open Russell
24
25type dAEMONXXX =
26| K1DAEMONXXX
27| K2DAEMONXXX
28
29val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
30
31val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
32
33val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
34
35val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
36
37val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
38
39val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
40
41val dAEMONXXX_inv_rect_Type4 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
42
43val dAEMONXXX_inv_rect_Type3 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
44
45val dAEMONXXX_inv_rect_Type2 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
46
47val dAEMONXXX_inv_rect_Type1 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
48
49val dAEMONXXX_inv_rect_Type0 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
50
51val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __
52
53val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __
54
55val ltb : Nat.nat -> Nat.nat -> Bool.bool
56
57val geb : Nat.nat -> Nat.nat -> Bool.bool
58
59val gtb : Nat.nat -> Nat.nat -> Bool.bool
60
61val eq_nat : Nat.nat -> Nat.nat -> Bool.bool
62
63val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
64
65val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list
66
67val fold_left2 :
68  ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list -> 'a1
69
70val remove_n_first_internal :
71  Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list
72
73val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list
74
75val foldi_from_until_internal :
76  Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
77  List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list
78
79val foldi_from_until :
80  Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) ->
81  'a1 List.list -> 'a1 List.list -> 'a1 List.list
82
83val foldi_from :
84  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
85  List.list -> 'a1 List.list -> 'a1 List.list
86
87val foldi_until :
88  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
89  List.list -> 'a1 List.list -> 'a1 List.list
90
91val foldi :
92  (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list -> 'a1
93  List.list -> 'a1 List.list
94
95val hd_safe : 'a1 List.list -> 'a1
96
97val tail_safe : 'a1 List.list -> 'a1 List.list
98
99val safe_split :
100  'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod
101
102val nth_safe : Nat.nat -> 'a1 List.list -> 'a1
103
104val last_safe : 'a1 List.list -> 'a1
105
106val reduce :
107  'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
108  Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
109
110val reduce_strong :
111  'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
112  Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
113  Types.sig0
114
115val map2_opt :
116  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
117  Types.option
118
119val map2 :
120  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
121
122val map3 :
123  ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
124  List.list -> 'a4 List.list
125
126val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
127
128val safe_nth : Nat.nat -> 'a1 List.list -> 'a1
129
130val nub_by_internal :
131  ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list
132
133val nub_by : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
134
135val member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool
136
137val take : Nat.nat -> 'a1 List.list -> 'a1 List.list
138
139val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list
140
141val list_split :
142  Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod
143
144val mapi_internal :
145  Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
146
147val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
148
149val zip_pottier :
150  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
151
152val zip_safe :
153  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
154
155val zip :
156  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
157  Types.option
158
159val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
160
161val rev : 'a1 List.list -> 'a1 List.list
162
163val fold_left_i_aux :
164  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1
165
166val fold_left_i :
167  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
168
169val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2
170
171val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1
172
173val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
174
175val division : Nat.nat -> Nat.nat -> Nat.nat
176
177val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
178
179val modulus : Nat.nat -> Nat.nat -> Nat.nat
180
181val divide_with_remainder :
182  Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod
183
184val less_than_or_equal_b_elim :
185  Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
186
187open Div_and_mod
188
189val dpi1__o__bool_to_Prop__o__inject :
190  (Bool.bool, 'a1) Types.dPair -> __ Types.sig0
191
192val eject__o__bool_to_Prop__o__inject : Bool.bool Types.sig0 -> __ Types.sig0
193
194val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0
195
196val dpi1__o__bool_to_Prop_to_eq__o__inject :
197  Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
198
199val eject__o__bool_to_Prop_to_eq__o__inject :
200  Bool.bool -> __ Types.sig0 -> __ Types.sig0
201
202val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
203
204val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
205  Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0
206
207val eject__o__not_bool_to_Prop_to_eq__o__inject :
208  Bool.bool -> __ Types.sig0 -> __ Types.sig0
209
210val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0
211
212val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
213
214val dpi1__o__not_neq_None__o__inject :
215  'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0
216
217val eject__o__not_neq_None__o__inject :
218  'a1 Types.option -> __ Types.sig0 -> __ Types.sig0
219
220val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0
221
222val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
223
224val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
225
226val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
227
228val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2
229
230val eq_sum :
231  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
232  Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool
233
234val eq_prod :
235  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
236  Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool
237
Note: See TracBrowser for help on using the repository browser.