val parse32_ifthenelse
      (p: parse_ifthenelse_param)
      (pt32: parser32 p.parse_ifthenelse_tag_parser)
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (pp32: (b: bool -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b)))))
      (synt:
          (
                b: bool ->
                t: p.parse_ifthenelse_tag_t{b == p.parse_ifthenelse_tag_cond t} ->
                pl: p.parse_ifthenelse_payload_t b
              -> Tot (y: p.parse_ifthenelse_t{y == p.parse_ifthenelse_synth t pl})))
    : Tot (parser32 (parse_ifthenelse p))
let parse32_ifthenelse
  (p: parse_ifthenelse_param)
  (pt32: parser32 p.parse_ifthenelse_tag_parser)
  (b32: (t: p.parse_ifthenelse_tag_t) -> Tot (b: bool { b == p.parse_ifthenelse_tag_cond t } ))
  (pp32: (b: bool) -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b))))
  (synt: (b: bool) -> (t: p.parse_ifthenelse_tag_t { b == p.parse_ifthenelse_tag_cond t } ) -> (pl: p.parse_ifthenelse_payload_t b) -> Tot (y: p.parse_ifthenelse_t { y == p.parse_ifthenelse_synth t pl } ))
: Tot (parser32 (parse_ifthenelse p))
= fun input ->
  ((
    [@inline_let]
    let _ = parse_ifthenelse_eq p (B32.reveal input) in
    match pt32 input with
    | None -> None
    | Some (t, consumed_t) ->
      let b = b32 t in
      let input' = B32.slice input consumed_t (B32.len input) in
      if b
      then
        match pp32 true input' with
        | None -> None
        | Some (pl, consumed_pl) ->
          Some (synt true t pl, consumed_t `U32.add` consumed_pl)
      else
        match pp32 false input' with
        | None -> None
        | Some (pl, consumed_pl) ->
          Some (synt false t pl, consumed_t `U32.add` consumed_pl)
  ) <: (res: _ { parser32_correct (parse_ifthenelse p) input res } )
  )
val parse32_ifthenelse
      (p: parse_ifthenelse_param)
      (pt32: parser32 p.parse_ifthenelse_tag_parser)
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (pp32: (b: bool -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b)))))
      (synt:
          (
                b: bool ->
                t: p.parse_ifthenelse_tag_t{b == p.parse_ifthenelse_tag_cond t} ->
                pl: p.parse_ifthenelse_payload_t b
              -> Tot (y: p.parse_ifthenelse_t{y == p.parse_ifthenelse_synth t pl})))
    : Tot (parser32 (parse_ifthenelse p))
let parse32_ifthenelse
      (p: parse_ifthenelse_param)
      (pt32: parser32 p.parse_ifthenelse_tag_parser)
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (pp32: (b: bool -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b)))))
      (synt:
          (
                b: bool ->
                t: p.parse_ifthenelse_tag_t{b == p.parse_ifthenelse_tag_cond t} ->
                pl: p.parse_ifthenelse_payload_t b
              -> Tot (y: p.parse_ifthenelse_t{y == p.parse_ifthenelse_synth t pl})))
    : Tot (parser32 (parse_ifthenelse p)) =
fun input ->
  (([@@ inline_let ]let _ = parse_ifthenelse_eq p (B32.reveal input) in
      match pt32 input with
      | None -> None
      | Some (t, consumed_t) ->
        let b = b32 t in
        let input' = B32.slice input consumed_t (B32.len input) in
        if b
        then
          match pp32 true input' with
          | None -> None
          | Some (pl, consumed_pl) -> Some (synt true t pl, consumed_t `U32.add` consumed_pl)
        else
          match pp32 false input' with
          | None -> None
          | Some (pl, consumed_pl) -> Some (synt false t pl, consumed_t `U32.add` consumed_pl))
    <:
    (res: _{parser32_correct (parse_ifthenelse p) input res}))
LowParse.SLow.IfThenElse.fst.checked
prims.fst.checked LowParse.Spec.IfThenElse.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.IfThenElse.fst
LowParse.Spec.IfThenElse.parse_ifthenelse_param LowParse.SLow.Base.parser32 LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_kind LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_parser Prims.bool Prims.eq2 LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_cond Prims.__proj__Mkdtuple2__item___1 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_parser FStar.Pervasives.dsnd LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_synth LowParse.SLow.Base.bytes32 FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 FStar.UInt32.t FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.UInt32.add FStar.Pervasives.Native.option LowParse.SLow.Base.parser32_correct LowParse.Spec.IfThenElse.parse_ifthenelse_kind LowParse.Spec.IfThenElse.parse_ifthenelse FStar.Bytes.bytes FStar.Seq.Base.seq FStar.UInt8.t FStar.Bytes.reveal FStar.Seq.Base.slice FStar.UInt32.v FStar.Bytes.len FStar.Bytes.slice Prims.unit LowParse.Spec.IfThenElse.parse_ifthenelse_eq
module LowParse.SLow.IfThenElse
include LowParse.Spec.IfThenElse
include LowParse.SLow.Combinators

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

inline_for_extraction
let parse32_ifthenelse
  (p: parse_ifthenelse_param)
  (pt32: parser32 p.parse_ifthenelse_tag_parser)
  (b32: (t: p.parse_ifthenelse_tag_t) -> Tot (b: bool { b == p.parse_ifthenelse_tag_cond t } ))
  (pp32: (b: bool) -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b))))
  (synt: (b: bool) -> (t: p.parse_ifthenelse_tag_t { b == p.parse_ifthenelse_tag_cond t } ) -> (pl: p.parse_ifthenelse_payload_t b) -> Tot (y: p.parse_ifthenelse_t { y == p.parse_ifthenelse_synth t pl } ))
val parse32_ifthenelse
      (p: parse_ifthenelse_param)
      (pt32: parser32 p.parse_ifthenelse_tag_parser)
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (pp32: (b: bool -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b)))))
      (synt:
          (
                b: bool ->
                t: p.parse_ifthenelse_tag_t{b == p.parse_ifthenelse_tag_cond t} ->
                pl: p.parse_ifthenelse_payload_t b
              -> Tot (y: p.parse_ifthenelse_t{y == p.parse_ifthenelse_synth t pl})))
    : Tot (parser32 (parse_ifthenelse p))

    p: LowParse.Spec.IfThenElse.parse_ifthenelse_param ->
    pt32: LowParse.SLow.Base.parser32 (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p) ->
    b32:
      (t: Mkparse_ifthenelse_param?.parse_ifthenelse_tag_t p
          -> b: Prims.bool{b == Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t}) ->
    pp32:
      (b: Prims.bool
          -> LowParse.SLow.Base.parser32 (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                      p
                      b))) ->
    synt:
      (
            b: Prims.bool ->
            t:
              Mkparse_ifthenelse_param?.parse_ifthenelse_tag_t p
                {b == Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t} ->
            pl: Mkparse_ifthenelse_param?.parse_ifthenelse_payload_t p b
          -> y:
            Mkparse_ifthenelse_param?.parse_ifthenelse_t p
              {y == Mkparse_ifthenelse_param?.parse_ifthenelse_synth p t pl})
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.IfThenElse.parse_ifthenelse p)