source: extracted/list.mli @ 2746

Last change on this file since 2746 was 2649, checked in by sacerdot, 7 years ago

...

File size: 3.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19type 'a list =
20| Nil
21| Cons of 'a * 'a list
22
23val list_rect_Type4 :
24  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
25
26val list_rect_Type3 :
27  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
28
29val list_rect_Type2 :
30  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
31
32val list_rect_Type1 :
33  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
34
35val list_rect_Type0 :
36  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
37
38val list_inv_rect_Type4 :
39  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
40  'a2
41
42val list_inv_rect_Type3 :
43  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
44  'a2
45
46val list_inv_rect_Type2 :
47  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
48  'a2
49
50val list_inv_rect_Type1 :
51  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
52  'a2
53
54val list_inv_rect_Type0 :
55  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
56  'a2
57
58val list_discr : 'a1 list -> 'a1 list -> __
59
60val append : 'a1 list -> 'a1 list -> 'a1 list
61
62val hd : 'a1 list -> 'a1 -> 'a1
63
64val tail : 'a1 list -> 'a1 list
65
66val option_hd : 'a1 list -> 'a1 Types.option
67
68val option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list
69
70val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
71
72val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2
73
74val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list
75
76val compose0 : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list
77
78val rev_append : 'a1 list -> 'a1 list -> 'a1 list
79
80val reverse : 'a1 list -> 'a1 list
81
82val length : 'a1 list -> Nat.nat
83
84type mem = __
85
86val split_rev :
87  'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
88
89val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
90
91val flatten : 'a1 list list -> 'a1 list
92
93val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1
94
95val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option
96
97type all = __
98
99type allr = __
100
101type exists = __
102
103val fold :
104  ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
105  list -> 'a2
106
107type 'a aop =
108  'a -> 'a -> 'a
109  (* singleton inductive, whose constructor was mk_Aop *)
110
111val aop_rect_Type4 :
112  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
113
114val aop_rect_Type5 :
115  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
116
117val aop_rect_Type3 :
118  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
119
120val aop_rect_Type2 :
121  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
122
123val aop_rect_Type1 :
124  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
125
126val aop_rect_Type0 :
127  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
128
129val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
130
131val aop_inv_rect_Type4 :
132  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
133  'a2
134
135val aop_inv_rect_Type3 :
136  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
137  'a2
138
139val aop_inv_rect_Type2 :
140  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
141  'a2
142
143val aop_inv_rect_Type1 :
144  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
145  'a2
146
147val aop_inv_rect_Type0 :
148  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
149  'a2
150
151val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
152
153val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
154
155val lhd : 'a1 list -> Nat.nat -> 'a1 list
156
157val ltl : 'a1 list -> Nat.nat -> 'a1 list
158
159val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option
160
161val position_of_aux :
162  ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option
163
164val position_of : ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option
165
166val make_list : 'a1 -> Nat.nat -> 'a1 list
167
Note: See TracBrowser for help on using the repository browser.