val parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p)
    : Tot (parser32 (parse_option p))
let parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p) : Tot (parser32 (parse_option p)) =
  fun input -> ((match p32 input with
  | Some (x, consumed) -> Some (Some x, consumed)
  | _ -> Some (None, 0ul)) <: (y: option (option t * U32.t) { parser32_correct (parse_option p) input y } ))
val parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p)
    : Tot (parser32 (parse_option p))
let parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p)
    : Tot (parser32 (parse_option p)) =
fun input ->
  ((match p32 input with
      | Some (x, consumed) -> Some (Some x, consumed)
      | _ -> Some (None, 0ul))
    <:
    (y: option (option t * U32.t) {parser32_correct (parse_option p) input y}))
LowParse.SLow.Option.fst.checked
prims.fst.checked LowParse.Spec.Option.fst.checked LowParse.SLow.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
LowParse.SLow.Option.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.SLow.Base.parser32 LowParse.SLow.Base.bytes32 FStar.UInt32.t FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.None FStar.UInt32.__uint_to_t LowParse.SLow.Base.parser32_correct LowParse.Spec.Option.parse_option_kind LowParse.Spec.Option.parse_option
module LowParse.SLow.Option
include LowParse.Spec.Option
include LowParse.SLow.Base

module U32 = FStar.UInt32
module B32 = FStar.Bytes

inline_for_extraction
val parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p)
    : Tot (parser32 (parse_option p))
p32: LowParse.SLow.Base.parser32 p
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.Option.parse_option p)