val parse32_u8: parser32 parse_u8
let parse32_u8 =
  decode_u8_injective ();
  make_total_constant_size_parser32 1 1ul
    decode_u8
    ()
    (fun (b: B32.lbytes 1) ->
      let r = B32.get b 0ul in
      assert (r == Seq.index (B32.reveal b) 0);
      B32.b32_index_reveal b 0;
      (r <: (y: U8.t { y == decode_u8 (B32.reveal b) })))
val parse32_u8: parser32 parse_u8
let parse32_u8 =
decode_u8_injective ();
make_total_constant_size_parser32 1
  1ul
  decode_u8
  ()
  (fun (b: B32.lbytes 1) ->
      let r = B32.get b 0ul in
      assert (r == Seq.index (B32.reveal b) 0);
      B32.b32_index_reveal b 0;
      (r <: (y: U8.t{y == decode_u8 (B32.reveal b)})))
LowParse.SLow.Int.fst.checked
prims.fst.checked LowParse.Spec.Int.fst.checked LowParse.Spec.Endianness.Instances.fst.checked LowParse.SLow.Endianness.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.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
LowParse.SLow.Int.fst
LowParse.SLow.Combinators.make_total_constant_size_parser32 FStar.UInt32.__uint_to_t FStar.UInt8.t LowParse.Spec.Int.decode_u8 FStar.Bytes.lbytes Prims.eq2 FStar.Bytes.reveal Prims.unit LowParse.Bytes32.b32_index_reveal Prims._assert FStar.Bytes.byte FStar.Seq.Base.index FStar.Bytes.get LowParse.Spec.Int.decode_u8_injective
module LowParse.SLow.Int
open LowParse.SLow.Combinators

module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module B32 = LowParse.Bytes32

friend LowParse.Spec.Int
val parse32_u8: parser32 parse_u8
LowParse.SLow.Base.parser32 LowParse.Spec.Int.parse_u8