val parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0)
let parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0) =
  feq _ _ (eq2 #_)
val parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0)
let parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0) =
feq _ _ (eq2 #_)
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.Enum.feq LowParse.SLow.Base.bytes32 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Sum.sum_type FStar.UInt32.t Prims.eq2 LowParse.SLow.Sum.parse32_sum_t
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))
val parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0)

    t: LowParse.Spec.Sum.sum ->
    _: LowParse.SLow.Sum.parse32_sum_t t ->
    _: LowParse.SLow.Sum.parse32_sum_t t
  -> Prims.GTot Type0