val decode_u8 (b: bytes{Seq.length b == 1}) : Tot U8.t
let decode_u8
  (b: bytes { Seq.length b == 1 } )
: Tot U8.t
= Seq.index b 0
val decode_u8 (b: bytes{Seq.length b == 1}) : Tot U8.t
let decode_u8 (b: bytes{Seq.length b == 1}) : Tot U8.t =
Seq.index b 0
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.Bytes.bytes Prims.eq2 Prims.int FStar.Seq.Base.length LowParse.Bytes.byte FStar.Seq.Base.index FStar.UInt8.t
module LowParse.Spec.Int
open LowParse.Spec.Combinators

let decode_u8
  (b: bytes { Seq.length b == 1 } )
val decode_u8 (b: bytes{Seq.length b == 1}) : Tot U8.t
b: LowParse.Bytes.bytes{FStar.Seq.Base.length b == 1} -> FStar.UInt8.t