val length (#a: Type0) (#len: flen) (s: ntuple a len) : flen
let length (#a:Type0) (#len:flen) (s: ntuple a len) : flen = len
val length (#a: Type0) (#len: flen) (s: ntuple a len) : flen
let length (#a: Type0) (#len: flen) (s: ntuple a len) : flen =
len
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
Lib.NTuple.flen Lib.NTuple.ntuple
module Lib.NTuple

open FStar.Mul
open Lib.IntTypes

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

let max_ntuple_len = max_size_t
val length (#a: Type0) (#len: flen) (s: ntuple a len) : flen
s: Lib.NTuple.ntuple a len -> Lib.NTuple.flen