source: extracted/vector.mli @ 2967

Last change on this file since 2967 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: 5.0 KB
RevLine 
[2601]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 Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
[2773]29open Setoids
30
31open Monad
32
33open Option
34
[2601]35open Extranat
36
37type 'a vector =
38| VEmpty
39| VCons of Nat.nat * 'a * 'a vector
40
41val vector_rect_Type4 :
42  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
43  vector -> 'a2
44
45val vector_rect_Type3 :
46  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
47  vector -> 'a2
48
49val vector_rect_Type2 :
50  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
51  vector -> 'a2
52
53val vector_rect_Type1 :
54  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
55  vector -> 'a2
56
57val vector_rect_Type0 :
58  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
59  vector -> 'a2
60
61val vector_inv_rect_Type4 :
62  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
63  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
64
65val vector_inv_rect_Type3 :
66  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
67  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
68
69val vector_inv_rect_Type2 :
70  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
71  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
72
73val vector_inv_rect_Type1 :
74  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
75  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
76
77val vector_inv_rect_Type0 :
78  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
79  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
80
81val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
82
83val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
84
85val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1
86
87val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1
88
89val get_index_weak_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option
90
91val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector
92
93val set_index_weak :
94  Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option
95
[2773]96val drop : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option
[2601]97
98val head' : Nat.nat -> 'a1 vector -> 'a1
99
[2773]100val tail : Nat.nat -> 'a1 vector -> 'a1 vector
[2601]101
102val vsplit' :
103  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
104
105val vsplit :
106  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
107
108val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod
109
110val from_singl : 'a1 vector -> 'a1
111
112val fold_right : Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
113
114val fold_right_i :
115  Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
116
117val fold_right2_i :
118  (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
119  'a2 vector -> 'a3
120
121val fold_left : Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1
122
[2773]123val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector
[2601]124
125val zip_with :
126  Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector
127
[2773]128val zip : Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector
[2601]129
130val replicate : Nat.nat -> 'a1 -> 'a1 vector
131
[2773]132val append : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
[2601]133
134val scan_left :
135  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector
136
137val scan_right :
138  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list
139
140val revapp : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
141
[2773]142val reverse : Nat.nat -> 'a1 vector -> 'a1 vector
[2601]143
144val pad_vector : 'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
145
146val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list
147
148val vector_of_list : 'a1 List.list -> 'a1 vector
149
150val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
151
152val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
153
154val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
155
156val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
157
158val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
159
160val shift_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
161
162val shift_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
163
164val eq_v :
165  Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
166  Bool.bool
167
168val vector_inv_n : Nat.nat -> 'a1 vector -> __
169
170val eq_v_elim :
171  ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ -> __)
172  -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__ -> 'a1)
173  -> 'a1
174
[2773]175val mem :
[2601]176  ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool
177
178val subvector_with :
179  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
180  -> Bool.bool
181
182val vprefix :
183  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
184  -> Bool.bool
185
186val vsuffix :
187  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
188  -> Bool.bool
189
190val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector
191
192val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector
193
Note: See TracBrowser for help on using the repository browser.