val parse_fldata'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Tot (bare_parser t)
let parse_fldata' #k #t p sz =
  let () = () in // Necessary to pass arity checking
  fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else
    match parse p (Seq.slice s 0 sz) with
    | Some (v, consumed) ->
      if (consumed <: nat) = (sz <: nat)
      then Some (v, (sz <: consumed_length s))
      else None
    | _ -> None
val parse_fldata'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Tot (bare_parser t)
let parse_fldata' #k #t p sz =
let () = () in
fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else
    match parse p (Seq.slice s 0 sz) with
    | Some (v, consumed) ->
      if (consumed <: nat) = (sz <: nat) then Some (v, (sz <: consumed_length s)) else None
    | _ -> None
LowParse.Spec.FLData.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.FLData.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Prims.nat LowParse.Bytes.bytes Prims.op_LessThan FStar.Seq.Base.length LowParse.Bytes.byte FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length Prims.bool LowParse.Spec.Base.parse FStar.Seq.Base.slice Prims.op_Equality FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option LowParse.Spec.Base.bare_parser Prims.unit
(* Parse data of some explicitly fixed length *)

module LowParse.Spec.FLData
include LowParse.Spec.Combinators

module Seq = FStar.Seq
module Classical = FStar.Classical

inline_for_extraction
val parse_fldata'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Tot (bare_parser t)
val parse_fldata'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Tot (bare_parser t)
p: LowParse.Spec.Base.parser k t -> sz: Prims.nat -> LowParse.Spec.Base.bare_parser t