val createi_ (#a: Type0) (min: nat) (max: flen{max > min}) (f: (i: nat{i < max} -> a))
    : Tot (ntuple_ a (max - min)) (decreases (max - min))
let rec createi_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> a)) :
  Tot (ntuple_ a (max - min)) (decreases (max - min))
 =
  if min + 1 = max then f min
  else f min, createi_ #a (min+1) max f
val createi_ (#a: Type0) (min: nat) (max: flen{max > min}) (f: (i: nat{i < max} -> a))
    : Tot (ntuple_ a (max - min)) (decreases (max - min))
let rec createi_ (#a: Type0) (min: nat) (max: flen{max > min}) (f: (i: nat{i < max} -> a))
    : Tot (ntuple_ a (max - min)) (decreases (max - min)) =
if min + 1 = max then f min else f min, createi_ #a (min + 1) max f
Lib.NTuple.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Lib.NTuple.fst
Prims.nat Lib.NTuple.flen Prims.b2t Prims.op_GreaterThan Prims.op_LessThan Prims.op_Equality Prims.int Prims.op_Addition Prims.bool FStar.Pervasives.Native.Mktuple2 Lib.NTuple.ntuple_ Prims.op_Subtraction Lib.NTuple.createi_
module Lib.NTuple

open FStar.Mul
open Lib.IntTypes

#set-options "--z3rlimit 15 --ifuel 0 --fuel 1"

let max_ntuple_len = max_size_t

unfold let length (#a:Type0) (#len:flen) (s: ntuple a len) : flen = len

inline_for_extraction
let fst_ (#a:Type0) (#len:flen) (s:ntuple_ a len) : a =
  if len = 1 then s
  else fst (s <: a & ntuple_ a (len - 1))

let fst #a #len (s:ntuple a len) =
  normalize_term (fst_ #a #len s)

inline_for_extraction
let rest_ (#a:Type0) (#len:flen{len > 1}) (s:ntuple_ a len) : ntuple_ a (len - 1)=
    snd (s <: a & ntuple_ a (len - 1))

let rest #a #len s =
  normalize_term (rest_ #a #len s)

inline_for_extraction
let rec index_ (#a:Type0) (#len:flen) (s:ntuple a len) (i:nat{i < len}) =
  if i = 0 then fst s
  else (assert (len > 1);
        index_ #a #(len-1) (rest s) (i-1))

let index #a #len s i =
  normalize_term (index_ s i)

let index_fst_lemma #a #len s = ()

inline_for_extraction
let rec createi_ (#a:Type0) (min:nat) (max:flen{max > min}) (f:(i:nat{i < max} -> a)) :
  Tot (ntuple_ a (max - min)) (decreases (max - min))
val createi_ (#a: Type0) (min: nat) (max: flen{max > min}) (f: (i: nat{i < max} -> a))
    : Tot (ntuple_ a (max - min)) (decreases (max - min))
min: Prims.nat -> max: Lib.NTuple.flen{max > min} -> f: (i: Prims.nat{i < max} -> a)
  -> Prims.Tot (Lib.NTuple.ntuple_ a (max - min))