val parse_seq_flbytes (sz: nat)
    : Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
let parse_seq_flbytes
  (sz: nat)
: Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
= tot_parse_seq_flbytes sz
val parse_seq_flbytes (sz: nat)
    : Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
let parse_seq_flbytes (sz: nat)
    : Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz)) =
tot_parse_seq_flbytes sz
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 LowParse.Spec.SeqBytes.Base.tot_parse_seq_flbytes LowParse.Spec.Base.parser LowParse.Spec.Base.total_constant_size_parser_kind FStar.Seq.Properties.lseq LowParse.Bytes.byte
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)
val parse_seq_flbytes (sz: nat)
    : Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
sz: Prims.nat
  -> LowParse.Spec.Base.parser (LowParse.Spec.Base.total_constant_size_parser_kind sz)
      (FStar.Seq.Properties.lseq LowParse.Bytes.byte sz)