val read_u8: leaf_reader parse_u8
let read_u8 : leaf_reader parse_u8 =
  decode_u8_injective ();
  leaf_reader_ext
    (make_total_constant_size_reader 1 1ul
      decode_u8
      ()
      (fun #rrel #rel b pos -> B.index b pos)
    )
    _
    (fun _ -> ())
val read_u8: leaf_reader parse_u8
let read_u8:leaf_reader parse_u8 =
decode_u8_injective ();
leaf_reader_ext (make_total_constant_size_reader 1
      1ul
      decode_u8
      ()
      (fun #rrel #rel b pos -> B.index b pos))
  _
  (fun _ -> ())
LowParse.Low.Int.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Int.fst.checked LowParse.Low.Endianness.fst.checked LowParse.Low.Combinators.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked
LowParse.Low.Int.fst
LowParse.Low.Base.leaf_reader_ext LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Bytes.byte LowParse.Spec.Combinators.make_total_constant_size_parser LowParse.Spec.Int.decode_u8 LowParse.Low.Combinators.make_total_constant_size_reader FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.srel LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t LowStar.Monotonic.Buffer.index LowParse.Spec.Int.parse_u8_kind LowParse.Spec.Int.parse_u8 LowParse.Bytes.bytes Prims.unit LowParse.Spec.Int.decode_u8_injective LowParse.Low.Base.leaf_reader FStar.UInt8.t
module LowParse.Low.Int
open LowParse.Low.Combinators

module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module E = FStar.Endianness
module LE = LowParse.Low.Endianness

friend LowParse.Spec.Int
val read_u8: leaf_reader parse_u8
LowParse.Low.Base.leaf_reader LowParse.Spec.Int.parse_u8