val serializer32_sum_gen_precond (kt k: parser_kind) : GTot Type0
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
  )
val serializer32_sum_gen_precond (kt k: parser_kind) : GTot Type0
let serializer32_sum_gen_precond (kt 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)
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.Base.parser_kind Prims.l_and Prims.eq2 FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.nat LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_high Prims.op_LessThan Prims.op_Addition Prims.logical
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)
val serializer32_sum_gen_precond (kt k: parser_kind) : GTot Type0
kt: LowParse.Spec.Base.parser_kind -> k: LowParse.Spec.Base.parser_kind -> Prims.GTot Type0