let vec_index (w:width) = n:size_t{v n < w}
let vec_index (w: width) =
n: size_t{v n < w}
Lib.IntVector.fsti.checked
Spec.AES.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Lib.IntVector.fsti
Lib.IntVector.width Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB
module Lib.IntVector

open FStar.Mul
open Lib.Sequence
open Lib.IntTypes

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"

let v_inttype = t:inttype{unsigned t /\ ~(U1? t)}
val vec_index : w: Lib.IntVector.width -> Type0
w: Lib.IntVector.width -> Type0