val parse32_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata p sz))
let parse32_fldata
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
: Tot (parser32 (parse_fldata p sz))
= (fun (input: bytes32) -> ((
    if U32.lt (B32.len input) sz32
    then
      None
    else
      match p32 (B32.b32slice input 0ul sz32) with
      | Some (v, consumed) ->
	if consumed = sz32
	then begin
	  Some (v, consumed)
	end else None
      | None -> None
  ) <: (res: option (t * U32.t) { parser32_correct (parse_fldata p sz) input res } )))
val parse32_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata p sz))
let parse32_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata p sz)) =
(fun (input: bytes32) ->
    ((if U32.lt (B32.len input) sz32
        then None
        else
          match p32 (B32.b32slice input 0ul sz32) with
          | Some (v, consumed) -> if consumed = sz32 then Some (v, consumed) else None
          | None -> None)
      <:
      (res: option (t * U32.t) {parser32_correct (parse_fldata p sz) input res})))
LowParse.SLow.FLData.fst.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.FLData.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.SLow.Base.parser32 Prims.nat FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v LowParse.SLow.Base.bytes32 FStar.UInt32.lt FStar.Bytes.len FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 Prims.bool LowParse.Bytes32.b32slice FStar.UInt32.__uint_to_t Prims.op_Equality FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option LowParse.SLow.Base.parser32_correct LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.FLData.parse_fldata
module LowParse.SLow.FLData
include LowParse.Spec.FLData
include LowParse.SLow.Combinators

module B32 = LowParse.Bytes32
module U32 = FStar.UInt32

inline_for_extraction
let parse32_fldata
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
val parse32_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata p sz))

    p32: LowParse.SLow.Base.parser32 p ->
    sz: Prims.nat ->
    sz32: FStar.UInt32.t{FStar.UInt32.v sz32 == sz}
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.FLData.parse_fldata p sz)