val parse_ifthenelse_payload_kind (p: parse_ifthenelse_param) : Tot parser_kind
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))
val parse_ifthenelse_payload_kind (p: parse_ifthenelse_param) : Tot parser_kind
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))
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.Base.glb FStar.Pervasives.dfst 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
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)
val parse_ifthenelse_payload_kind (p: parse_ifthenelse_param) : Tot parser_kind
p: LowParse.Spec.IfThenElse.parse_ifthenelse_param -> LowParse.Spec.Base.parser_kind