val parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t)
    : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t)
let parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t) : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t) =
  weaken (parse_ifthenelse_payload_kind p) (parse_synth (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t))) (p.parse_ifthenelse_synth t))
val parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t)
    : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t)
let parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t)
    : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t) =
weaken (parse_ifthenelse_payload_kind p)
  (parse_synth (dsnd (p.parse_ifthenelse_payload_parser (p.parse_ifthenelse_tag_cond t)))
      (p.parse_ifthenelse_synth t))
LowParse.Spec.IfThenElse.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.IfThenElse.fst
LowParse.Spec.IfThenElse.parse_ifthenelse_param LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_t LowParse.Spec.Base.weaken LowParse.Spec.IfThenElse.parse_ifthenelse_payload_kind 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_tag_cond LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_parser LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_t LowParse.Spec.Combinators.parse_synth FStar.Pervasives.dsnd LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_synth
module LowParse.Spec.IfThenElse
include LowParse.Spec.Combinators

module Seq = FStar.Seq

[@@(noextract_to "krml")]
inline_for_extraction
noeq
type parse_ifthenelse_param = {
  parse_ifthenelse_tag_kind: parser_kind;
  parse_ifthenelse_tag_t: Type;
  parse_ifthenelse_tag_parser: parser parse_ifthenelse_tag_kind parse_ifthenelse_tag_t;
  parse_ifthenelse_tag_cond: (parse_ifthenelse_tag_t -> Tot bool);
  parse_ifthenelse_payload_t: (bool -> Tot Type);
  parse_ifthenelse_payload_parser: ((b: bool) -> Tot (k: parser_kind & parser k (parse_ifthenelse_payload_t b)));
  parse_ifthenelse_t: Type;
  parse_ifthenelse_synth: ((t: parse_ifthenelse_tag_t) -> (parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t)) -> GTot parse_ifthenelse_t);
  parse_ifthenelse_synth_injective: (
    (t1: parse_ifthenelse_tag_t) ->
    (x1: parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t1)) ->
    (t2: parse_ifthenelse_tag_t) ->
    (x2: parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t2)) ->
    Lemma
    (requires (parse_ifthenelse_synth t1 x1 == parse_ifthenelse_synth t2 x2))
              (ensures (t1 == t2 /\ coerce (parse_ifthenelse_payload_t (parse_ifthenelse_tag_cond t2)) x1 == x2))
  );
}

inline_for_extraction
let parse_ifthenelse_payload_kind
  (p: parse_ifthenelse_param)
: Tot parser_kind
= glb (dfst (p.parse_ifthenelse_payload_parser true)) (dfst (p.parse_ifthenelse_payload_parser false))

inline_for_extraction
let parse_ifthenelse_kind
  (p: parse_ifthenelse_param)
: Tot parser_kind
= and_then_kind p.parse_ifthenelse_tag_kind (parse_ifthenelse_payload_kind p)

let parse_ifthenelse_synth_injective (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t) : Lemma (synth_injective (p.parse_ifthenelse_synth t)) [SMTPat (synth_injective (p.parse_ifthenelse_synth t))] =
  Classical.forall_intro_2 (fun x1 x2 -> Classical.move_requires (p.parse_ifthenelse_synth_injective t x1 t) x2)
val parse_ifthenelse_payload (p: parse_ifthenelse_param) (t: p.parse_ifthenelse_tag_t)
    : Tot (parser (parse_ifthenelse_payload_kind p) p.parse_ifthenelse_t)

    p: LowParse.Spec.IfThenElse.parse_ifthenelse_param ->
    t: Mkparse_ifthenelse_param?.parse_ifthenelse_tag_t p
  -> LowParse.Spec.Base.parser (LowParse.Spec.IfThenElse.parse_ifthenelse_payload_kind p)
      (Mkparse_ifthenelse_param?.parse_ifthenelse_t p)