val parse32_sum_cases'
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (pc32: (x: sum_key t -> Tot (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases' t pc k))
let parse32_sum_cases'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (parser32 (dsnd (pc x)))))
  (k: sum_key t)
: Tot (parser32 (parse_sum_cases' t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
        parse32_synth'
            (dsnd (pc k))
            (synth_sum_case t k)
            (pc32 k)
            ()
val parse32_sum_cases'
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (pc32: (x: sum_key t -> Tot (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases' t pc k))
let parse32_sum_cases'
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (pc32: (x: sum_key t -> Tot (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases' t pc k)) =
[@@ inline_let ]let _ = synth_sum_case_injective t k in
parse32_synth' (dsnd (pc k)) (synth_sum_case t k) (pc32 k) ()
LowParse.SLow.Sum.fst.checked
prims.fst.checked LowParse.Spec.Sum.fst.checked LowParse.SLow.Enum.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.SLow.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 LowParse.SLow.Base.parser32 Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd LowParse.SLow.Combinators.parse32_synth' LowParse.Spec.Sum.sum_cases LowParse.Spec.Sum.synth_sum_case Prims.unit LowParse.Spec.Sum.synth_sum_case_injective FStar.Pervasives.dfst LowParse.Spec.Sum.parse_sum_cases'
module LowParse.SLow.Sum
include LowParse.Spec.Sum
include LowParse.SLow.Enum

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

let serializer32_sum_gen_precond
  (kt: parser_kind)
  (k: parser_kind)
: GTot Type0
= kt.parser_kind_subkind == Some ParserStrong /\
  Some? kt.parser_kind_high /\
  Some? k.parser_kind_high /\ (
  let (Some vt) = kt.parser_kind_high in
  let (Some v) = k.parser_kind_high in
  vt + v < 4294967296
  )

inline_for_extraction
let parse32_sum_t (t: sum) : Tot Type =
  bytes32 -> Tot (option (sum_type t * U32.t))

let parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0) =
  feq _ _ (eq2 #_)

inline_for_extraction
let parse32_sum_if (t: sum) : Tot (if_combinator _ (parse32_sum_eq t)) =
  fif _ _ _ (default_if _)

let parse32_sum_eq_refl (t: sum) : Tot (r_reflexive_t _ (parse32_sum_eq t)) =
  fun _ -> ()

let parse32_sum_eq_trans (t: sum) : Tot (r_transitive_t _ (parse32_sum_eq t)) = feq_trans _ _ (eq2 #_)

inline_for_extraction
let parse32_sum_cases'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (parser32 (dsnd (pc x)))))
  (k: sum_key t)
val parse32_sum_cases'
      (t: sum)
      (pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (pc32: (x: sum_key t -> Tot (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases' 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))) ->
    pc32:
      (x: LowParse.Spec.Sum.sum_key t -> LowParse.SLow.Base.parser32 (FStar.Pervasives.dsnd (pc x))) ->
    k: LowParse.Spec.Sum.sum_key t
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.Sum.parse_sum_cases' t pc k)