val parse_vlgen_weak_bare
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 min max))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
    : Tot (bare_parser t)
let parse_vlgen_weak_bare
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#sk: parser_kind)
  (pk: parser sk (bounded_int32 min max))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (bare_parser t)
= fun input ->
    match pk input with
    | None -> None
    | Some (len, sz) ->
      begin
        if Seq.length input < sz + U32.v len
        then None
        else
        let input' = Seq.slice input sz (sz + U32.v len) in
        match p input' with
        | Some (x, consumed_x) ->
          if consumed_x = U32.v len
          then
            Some (x, sz + U32.v len)
        else None
      | _ -> None
    end
val parse_vlgen_weak_bare
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 min max))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
    : Tot (bare_parser t)
let parse_vlgen_weak_bare
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 min max))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
    : Tot (bare_parser t) =
fun input ->
  match pk input with
  | None -> None
  | Some (len, sz) ->
    if Seq.length input < sz + U32.v len
    then None
    else
      let input' = Seq.slice input sz (sz + U32.v len) in
      match p input' with
      | Some (x, consumed_x) -> if consumed_x = U32.v len then Some (x, sz + U32.v len) else None
      | _ -> None
LowParse.Tot.VLGen.fst.checked
prims.fst.checked LowParse.Tot.Int.fst.checked LowParse.Tot.Combinators.fst.checked LowParse.Spec.VLGen.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Tot.VLGen.fst
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Spec.Base.parser_kind LowParse.Tot.Base.parser LowParse.Spec.BoundedInt.bounded_int32 LowParse.Bytes.bytes FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length FStar.Seq.Base.length LowParse.Bytes.byte Prims.op_Addition FStar.UInt32.v Prims.bool Prims.op_Equality Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option FStar.Seq.Base.seq FStar.Seq.Base.slice LowParse.Tot.Base.bare_parser
module LowParse.Tot.VLGen
include LowParse.Spec.VLGen
include LowParse.Tot.Int
include LowParse.Tot.Combinators

module U32 = FStar.UInt32

let parse_vlgen_weak_bare
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#sk: parser_kind)
  (pk: parser sk (bounded_int32 min max))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
val parse_vlgen_weak_bare
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 min max))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
    : Tot (bare_parser t)

    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max < 4294967296} ->
    pk: LowParse.Tot.Base.parser sk (LowParse.Spec.BoundedInt.bounded_int32 min max) ->
    p: LowParse.Tot.Base.parser k t
  -> LowParse.Tot.Base.bare_parser t