val read_bounded_integer (i: integer_size) : Tot (leaf_reader (parse_bounded_integer i))
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 ()
val read_bounded_integer (i: integer_size) : Tot (leaf_reader (parse_bounded_integer i))
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 ()
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
LowParse.Spec.BoundedInt.integer_size LowParse.Low.BoundedInt.read_bounded_integer_1 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.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer Prims.unit LowParse.Spec.BoundedInt.integer_size_values
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)
val read_bounded_integer (i: integer_size) : Tot (leaf_reader (parse_bounded_integer i))
i: LowParse.Spec.BoundedInt.integer_size
  -> LowParse.Low.Base.leaf_reader (LowParse.Spec.BoundedInt.parse_bounded_integer i)