val parse32_maybe_enum_key_gen
      (#k: parser_kind)
      (#key #repr: eqtype)
      (#p: parser k repr)
      (p32: parser32 p)
      (e: enum key repr)
      (k': parser_kind)
      (t': Type)
      (p': parser k' t')
      (u1: unit{k' == k})
      (u15: unit{t' == maybe_enum_key e})
      (u2: unit{p' == parse_maybe_enum_key p e})
      (f: maybe_enum_key_of_repr'_t e)
    : Tot (parser32 p')
let parse32_maybe_enum_key_gen
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (p32: parser32 p)
  (e: enum key repr)
  (k' : parser_kind)
  (t' : Type)
  (p' : parser k' t')
  (u1: unit { k' == k })
  (u15: unit { t' == maybe_enum_key e } )
  (u2: unit { p' == parse_maybe_enum_key p e } )
  (f: maybe_enum_key_of_repr'_t e)
: Tot (parser32 p')
= parse32_synth p (maybe_enum_key_of_repr e) f p32 ()
val parse32_maybe_enum_key_gen
      (#k: parser_kind)
      (#key #repr: eqtype)
      (#p: parser k repr)
      (p32: parser32 p)
      (e: enum key repr)
      (k': parser_kind)
      (t': Type)
      (p': parser k' t')
      (u1: unit{k' == k})
      (u15: unit{t' == maybe_enum_key e})
      (u2: unit{p' == parse_maybe_enum_key p e})
      (f: maybe_enum_key_of_repr'_t e)
    : Tot (parser32 p')
let parse32_maybe_enum_key_gen
      (#k: parser_kind)
      (#key #repr: eqtype)
      (#p: parser k repr)
      (p32: parser32 p)
      (e: enum key repr)
      (k': parser_kind)
      (t': Type)
      (p': parser k' t')
      (u1: unit{k' == k})
      (u15: unit{t' == maybe_enum_key e})
      (u2: unit{p' == parse_maybe_enum_key p e})
      (f: maybe_enum_key_of_repr'_t e)
    : Tot (parser32 p') =
parse32_synth p (maybe_enum_key_of_repr e) f p32 ()
LowParse.SLow.Enum.fst.checked
prims.fst.checked LowParse.Spec.Enum.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
LowParse.SLow.Enum.fst
LowParse.Spec.Base.parser_kind Prims.eqtype LowParse.Spec.Base.parser LowParse.SLow.Base.parser32 LowParse.Spec.Enum.enum Prims.unit Prims.eq2 LowParse.Spec.Enum.maybe_enum_key LowParse.Spec.Enum.parse_maybe_enum_key LowParse.Spec.Enum.maybe_enum_key_of_repr'_t LowParse.SLow.Combinators.parse32_synth LowParse.Spec.Enum.maybe_enum_key_of_repr
module LowParse.SLow.Enum
include LowParse.Spec.Enum
include LowParse.SLow.Combinators

module L = FStar.List.Tot
module U32 = FStar.UInt32

(* Parser for enums *)

inline_for_extraction
let parse32_maybe_enum_key_gen
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (p32: parser32 p)
  (e: enum key repr)
  (k' : parser_kind)
  (t' : Type)
  (p' : parser k' t')
  (u1: unit { k' == k })
  (u15: unit { t' == maybe_enum_key e } )
  (u2: unit { p' == parse_maybe_enum_key p e } )
  (f: maybe_enum_key_of_repr'_t e)
val parse32_maybe_enum_key_gen
      (#k: parser_kind)
      (#key #repr: eqtype)
      (#p: parser k repr)
      (p32: parser32 p)
      (e: enum key repr)
      (k': parser_kind)
      (t': Type)
      (p': parser k' t')
      (u1: unit{k' == k})
      (u15: unit{t' == maybe_enum_key e})
      (u2: unit{p' == parse_maybe_enum_key p e})
      (f: maybe_enum_key_of_repr'_t e)
    : Tot (parser32 p')

    p32: LowParse.SLow.Base.parser32 p ->
    e: LowParse.Spec.Enum.enum key repr ->
    k': LowParse.Spec.Base.parser_kind ->
    t': Type0 ->
    p': LowParse.Spec.Base.parser k' t' ->
    u1: Prims.unit{k' == k} ->
    u15: Prims.unit{t' == LowParse.Spec.Enum.maybe_enum_key e} ->
    u2: Prims.unit{p' == LowParse.Spec.Enum.parse_maybe_enum_key p e} ->
    f: LowParse.Spec.Enum.maybe_enum_key_of_repr'_t e
  -> LowParse.SLow.Base.parser32 p'