39 | VCons of Nat.nat * 'a * 'a vector
41 val vector_rect_Type4 :
42 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
45 val vector_rect_Type3 :
46 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
49 val vector_rect_Type2 :
50 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
53 val vector_rect_Type1 :
54 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
57 val vector_rect_Type0 :
58 'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
61 val vector_inv_rect_Type4 :
62 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
63 -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
65 val vector_inv_rect_Type3 :
66 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
67 -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
69 val vector_inv_rect_Type2 :
70 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
71 -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
73 val vector_inv_rect_Type1 :
74 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
75 -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
77 val vector_inv_rect_Type0 :
78 Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
79 -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
81 val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
83 val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
85 val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1
87 val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1
89 val get_index_weak_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option
91 val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector
94 Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option
96 val drop : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option
98 val head' : Nat.nat -> 'a1 vector -> 'a1
100 val tail : Nat.nat -> 'a1 vector -> 'a1 vector
103 Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
106 Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
108 val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod
110 val from_singl : 'a1 vector -> 'a1
112 val fold_right : Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
115 Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
118 (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
121 val fold_left : Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1
123 val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector
126 Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector
128 val zip : Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector
130 val replicate : Nat.nat -> 'a1 -> 'a1 vector
132 val append : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
135 Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector
138 Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list
140 val revapp : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
142 val reverse : Nat.nat -> 'a1 vector -> 'a1 vector
144 val pad_vector : 'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
146 val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list
148 val vector_of_list : 'a1 List.list -> 'a1 vector
150 val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
152 val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
154 val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
156 val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
158 val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
160 val shift_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
162 val shift_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
165 Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
168 val vector_inv_n : Nat.nat -> 'a1 vector -> __
171 ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ -> __)
172 -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__ -> 'a1)
176 ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool
179 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
183 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
187 Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
190 val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector
192 val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector