val validate_sum_cases_t_if
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (k: sum_key t)
    : Tot (if_combinator _ (validate_sum_cases_t_eq t pc k))
let validate_sum_cases_t_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot (if_combinator _ (validate_sum_cases_t_eq t pc k))
= fun cond (sv_true: cond_true cond -> Tot (validate_sum_cases_t t pc k)) (sv_false: cond_false cond -> Tot (validate_sum_cases_t t pc k)) #rrel #rel input pos ->
  if cond
  then sv_true () input pos
  else sv_false () input pos
val validate_sum_cases_t_if
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (k: sum_key t)
    : Tot (if_combinator _ (validate_sum_cases_t_eq t pc k))
let validate_sum_cases_t_if
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (k: sum_key t)
    : Tot (if_combinator _ (validate_sum_cases_t_eq t pc k)) =
fun
  cond
  (sv_true: (cond_true cond -> Tot (validate_sum_cases_t t pc k)))
  (sv_false: (cond_false cond -> Tot (validate_sum_cases_t t pc k)))
  #rrel
  #rel
  input
  pos
  ->
  if cond then sv_true () input pos else sv_false () input pos
LowParse.Low.Sum.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Sum.fst.checked LowParse.Low.Enum.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
LowParse.Low.Sum.fst
LowParse.Spec.Sum.sum LowParse.Spec.Sum.sum_key Prims.dtuple2 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Sum.sum_type_of_tag Prims.bool LowParse.Spec.Combinators.cond_true LowParse.Low.Sum.validate_sum_cases_t LowParse.Spec.Combinators.cond_false LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t LowParse.Spec.Enum.if_combinator LowParse.Low.Sum.validate_sum_cases_t_eq
module LowParse.Low.Sum
include LowParse.Low.Enum
include LowParse.Spec.Sum

module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

inline_for_extraction
let validate_sum_cases_aux
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (vc: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (k: sum_key t)
: Tot (validator (parse_sum_cases t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
  validate_synth
    (validate_weaken
      (weaken_parse_cases_kind t pc)
      (vc k)
      ()
    )
    (synth_sum_case t k)
    ()

inline_for_extraction
let validate_sum_cases_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot Type
= validator (parse_sum_cases t pc k)

let validate_sum_cases_t_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
  (x y : validate_sum_cases_t t pc k)
: GTot Type0
= True

inline_for_extraction
let validate_sum_cases_t_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
val validate_sum_cases_t_if
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (k: sum_key t)
    : Tot (if_combinator _ (validate_sum_cases_t_eq t pc k))

    t: LowParse.Spec.Sum.sum ->
    pc:
      (x: LowParse.Spec.Sum.sum_key t
          -> Prims.dtuple2 LowParse.Spec.Base.parser_kind
              (fun k -> LowParse.Spec.Base.parser k (LowParse.Spec.Sum.sum_type_of_tag t x))) ->
    k: LowParse.Spec.Sum.sum_key t
  -> LowParse.Spec.Enum.if_combinator (LowParse.Low.Sum.validate_sum_cases_t t pc k)
      (LowParse.Low.Sum.validate_sum_cases_t_eq t pc k)