val serialize_seq_flbytes' (sz: nat) : Tot (bare_serializer (Seq.lseq byte sz))
let serialize_seq_flbytes'
  (sz: nat)
: Tot (bare_serializer (Seq.lseq byte sz))
= fun (x: Seq.lseq byte sz) -> (
    x
  )
val serialize_seq_flbytes' (sz: nat) : Tot (bare_serializer (Seq.lseq byte sz))
let serialize_seq_flbytes' (sz: nat) : Tot (bare_serializer (Seq.lseq byte sz)) =
fun (x: Seq.lseq byte sz) -> (x)
LowParse.Spec.SeqBytes.Base.fst.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.SeqBytes.Base.fst
Prims.nat FStar.Seq.Properties.lseq LowParse.Bytes.byte LowParse.Bytes.bytes LowParse.Spec.Base.bare_serializer
module LowParse.Spec.SeqBytes.Base
include LowParse.Spec.FLData

let parse_seq_flbytes_gen
  (sz: nat)
  (s: bytes { Seq.length s == sz } )
: Tot (Seq.lseq byte sz)
= s

let tot_parse_seq_flbytes
  (sz: nat)
: Tot (tot_parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
= tot_make_total_constant_size_parser sz (Seq.lseq byte sz) (parse_seq_flbytes_gen sz)

let parse_seq_flbytes
  (sz: nat)
: Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
= tot_parse_seq_flbytes sz

let serialize_seq_flbytes'
  (sz: nat)
val serialize_seq_flbytes' (sz: nat) : Tot (bare_serializer (Seq.lseq byte sz))
sz: Prims.nat
  -> LowParse.Spec.Base.bare_serializer (FStar.Seq.Properties.lseq LowParse.Bytes.byte sz)