extracted/vector.mli

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