val tot_parse_u8: tot_parser parse_u8_kind U8.t
let tot_parse_u8 =
  decode_u8_injective ();
  tot_make_total_constant_size_parser 1 U8.t decode_u8
val tot_parse_u8: tot_parser parse_u8_kind U8.t
let tot_parse_u8 =
decode_u8_injective ();
tot_make_total_constant_size_parser 1 U8.t decode_u8
LowParse.Spec.Int.fst.checked
prims.fst.checked LowParse.Spec.Seq.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Int.fst
LowParse.Spec.Combinators.tot_make_total_constant_size_parser FStar.UInt8.t LowParse.Spec.Int.decode_u8 Prims.unit LowParse.Spec.Int.decode_u8_injective
module LowParse.Spec.Int
open LowParse.Spec.Combinators

let decode_u8
  (b: bytes { Seq.length b == 1 } )
: Tot U8.t
= Seq.index b 0

let decode_u8_injective () : Lemma
  (make_total_constant_size_parser_precond 1 U8.t decode_u8)
= ()
val tot_parse_u8: tot_parser parse_u8_kind U8.t
LowParse.Spec.Base.tot_parser LowParse.Spec.Int.parse_u8_kind FStar.UInt8.t