source: driver/extracted/list.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: 3.8 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 compose : ('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
84val split_rev :
85  'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
86
87val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
88
89val flatten : 'a1 list list -> 'a1 list
90
91val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1
92
93val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option
94
95val fold :
96  ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
97  list -> 'a2
98
99type 'a aop =
100  'a -> 'a -> 'a
101  (* singleton inductive, whose constructor was mk_Aop *)
102
103val aop_rect_Type4 :
104  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
105
106val aop_rect_Type5 :
107  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
108
109val aop_rect_Type3 :
110  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
111
112val aop_rect_Type2 :
113  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
114
115val aop_rect_Type1 :
116  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
117
118val aop_rect_Type0 :
119  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
120
121val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
122
123val aop_inv_rect_Type4 :
124  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
125  'a2
126
127val aop_inv_rect_Type3 :
128  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
129  'a2
130
131val aop_inv_rect_Type2 :
132  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
133  'a2
134
135val aop_inv_rect_Type1 :
136  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
137  'a2
138
139val aop_inv_rect_Type0 :
140  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
141  'a2
142
143val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
144
145val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
146
147val lhd : 'a1 list -> Nat.nat -> 'a1 list
148
149val ltl : 'a1 list -> Nat.nat -> 'a1 list
150
151val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option
152
153val position_of_aux :
154  ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option
155
156val position_of : ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option
157
158val make_list : 'a1 -> Nat.nat -> 'a1 list
159
Note: See TracBrowser for help on using the repository browser.