val read_bounded_integer' (i: U32.t{1 <= U32.v i /\ U32.v i <= 4})
    : Tot (leaf_reader (parse_bounded_integer (U32.v i)))
let read_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
: Tot (leaf_reader (parse_bounded_integer (U32.v i)))
= fun #rrel #rel sl pos ->
  if i = 1ul
  then read_bounded_integer_1 () sl pos
  else if i = 2ul
  then read_bounded_integer_2 () sl pos
  else if i = 3ul
  then read_bounded_integer_3 () sl pos
  else read_bounded_integer_4 () sl pos
val read_bounded_integer' (i: U32.t{1 <= U32.v i /\ U32.v i <= 4})
    : Tot (leaf_reader (parse_bounded_integer (U32.v i)))
let read_bounded_integer' (i: U32.t{1 <= U32.v i /\ U32.v i <= 4})
    : Tot (leaf_reader (parse_bounded_integer (U32.v i))) =
fun #rrel #rel sl pos ->
  if i = 1ul
  then read_bounded_integer_1 () sl pos
  else
    if i = 2ul
    then read_bounded_integer_2 () sl pos
    else if i = 3ul then read_bounded_integer_3 () sl pos else read_bounded_integer_4 () sl pos
LowParse.Low.BoundedInt.fsti.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowParse.Spec.BoundedInt.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked
LowParse.Low.BoundedInt.fsti
FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice Prims.op_Equality FStar.UInt32.__uint_to_t LowParse.Low.BoundedInt.read_bounded_integer_1 LowParse.Spec.BoundedInt.bounded_integer Prims.bool LowParse.Low.BoundedInt.read_bounded_integer_2 LowParse.Low.BoundedInt.read_bounded_integer_3 LowParse.Low.BoundedInt.read_bounded_integer_4 LowParse.Low.Base.leaf_reader LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer
module LowParse.Low.BoundedInt
include LowParse.Spec.BoundedInt
include LowParse.Low.Base

module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Monotonic.Buffer
module U64 = FStar.UInt64

(* bounded integers *)

inline_for_extraction
val read_bounded_integer_1 : unit -> Tot (leaf_reader (parse_bounded_integer 1))

inline_for_extraction
val read_bounded_integer_2 : unit -> Tot (leaf_reader (parse_bounded_integer 2))

inline_for_extraction
val read_bounded_integer_3 : unit -> Tot (leaf_reader (parse_bounded_integer 3))

inline_for_extraction
val read_bounded_integer_4 : unit -> Tot (leaf_reader (parse_bounded_integer 4))

inline_for_extraction
noextract
let read_bounded_integer
  (i: integer_size)
: Tot (leaf_reader (parse_bounded_integer i))
= [@inline_let]
  let _ = integer_size_values i in
  match i with
  | 1 -> read_bounded_integer_1 ()
  | 2 -> read_bounded_integer_2 ()
  | 3 -> read_bounded_integer_3 ()
  | 4 -> read_bounded_integer_4 ()

let read_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
val read_bounded_integer' (i: U32.t{1 <= U32.v i /\ U32.v i <= 4})
    : Tot (leaf_reader (parse_bounded_integer (U32.v i)))
i: FStar.UInt32.t{1 <= FStar.UInt32.v i /\ FStar.UInt32.v i <= 4}
  -> LowParse.Low.Base.leaf_reader (LowParse.Spec.BoundedInt.parse_bounded_integer (FStar.UInt32.v i
          ))