val enum_destr_cons
      (t: Type)
      (#key #repr: eqtype)
      (e: enum key repr)
      (g: enum_destr_t t (enum_tail' e))
    : Pure (enum_destr_t t e) (requires (Cons? e)) (ensures (fun _ -> True))
let enum_destr_cons
  (t: Type)
  (#key #repr: eqtype)
  (e: enum key repr)
  (g: enum_destr_t t (enum_tail' e))
: Pure (enum_destr_t t e)
  (requires (Cons? e))
  (ensures (fun _ -> True))
= fun (eq: (t -> t -> GTot Type0)) (ift: if_combinator t eq) (eq_refl: r_reflexive_t _ eq) (eq_trans: r_transitive_t _ eq) ->
  [@inline_let]
  let _ = r_reflexive_t_elim _ _ eq_refl in
  [@inline_let]
  let _ = r_transitive_t_elim _ _ eq_trans in
  (fun (e' : list (key * repr) { e' == e } ) -> match e' with
     | (k, _) :: _ ->
     (fun (f: (enum_key e -> Tot t)) (x: enum_key e) -> ((
       [@inline_let]
       let f' : (enum_key (enum_tail' e) -> Tot t) =
         (fun (x' : enum_key (enum_tail' e)) ->
           [@inline_let]
           let (x_ : enum_key e) = (x' <: key) in
           f x_
         )
       in
       [@inline_let]
       let (y: t) =
       ift
         ((k <: key) = x)
         (fun h -> f k)
         (fun h ->
           [@inline_let]
           let x' : enum_key (enum_tail' e) = (x <: key) in
           (g eq ift eq_refl eq_trans f' x' <: t))
       in
       y
     ) <: (y: t { eq y (f x) } )))
  ) e
val enum_destr_cons
      (t: Type)
      (#key #repr: eqtype)
      (e: enum key repr)
      (g: enum_destr_t t (enum_tail' e))
    : Pure (enum_destr_t t e) (requires (Cons? e)) (ensures (fun _ -> True))
let enum_destr_cons
      (t: Type)
      (#key #repr: eqtype)
      (e: enum key repr)
      (g: enum_destr_t t (enum_tail' e))
    : Pure (enum_destr_t t e) (requires (Cons? e)) (ensures (fun _ -> True)) =
fun
  (eq: (t -> t -> GTot Type0))
  (ift: if_combinator t eq)
  (eq_refl: r_reflexive_t _ eq)
  (eq_trans: r_transitive_t _ eq)
  ->
  [@@ inline_let ]let _ = r_reflexive_t_elim _ _ eq_refl in
  [@@ inline_let ]let _ = r_transitive_t_elim _ _ eq_trans in
  (fun (e': list (key * repr) {e' == e}) ->
      match e' with
      | (k, _) :: _ ->
        (fun (f: (enum_key e -> Tot t)) (x: enum_key e) ->
            (([@@ inline_let ]let f':(enum_key (enum_tail' e) -> Tot t) =
                  (fun (x': enum_key (enum_tail' e)) ->
                      [@@ inline_let ]let x_:enum_key e = (x' <: key) in
                      f x_)
                in
                [@@ inline_let ]let y:t =
                  ift ((k <: key) = x)
                    (fun h -> f k)
                    (fun h ->
                        [@@ inline_let ]let x':enum_key (enum_tail' e) = (x <: key) in
                        (g eq ift eq_refl eq_trans f' x' <: t))
                in
                y)
              <:
              (y: t{eq y (f x)})))) e
LowParse.Spec.Enum.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.Enum.fst
Prims.eqtype LowParse.Spec.Enum.enum LowParse.Spec.Enum.enum_destr_t LowParse.Spec.Enum.enum_tail' LowParse.Spec.Enum.if_combinator LowParse.Spec.Enum.r_reflexive_t LowParse.Spec.Enum.r_transitive_t Prims.list FStar.Pervasives.Native.tuple2 LowParse.Spec.Enum.enum_key Prims.op_Equality LowParse.Spec.Combinators.cond_true LowParse.Spec.Combinators.cond_false Prims.unit LowParse.Spec.Enum.r_transitive_t_elim LowParse.Spec.Enum.r_reflexive_t_elim Prims.b2t Prims.uu___is_Cons Prims.l_True
module LowParse.Spec.Enum
include LowParse.Spec.Combinators

module L = FStar.List.Tot

[@Norm]
let rec list_map
  (#a #b: Type)
  (f: (a -> Tot b))
  (l: list a)
: Tot (l' : list b { l' == L.map f l } )
= match l with
  | [] -> []
  | a :: q -> f a :: list_map f q

type enum (key: eqtype) (repr: eqtype) = (l: list (key * repr) {
  L.noRepeats (list_map fst l) /\
  L.noRepeats (list_map snd l)
})

[@Norm]
let rec list_mem
  (#t: eqtype)
  (x: t)
  (l: list t)
: Tot (y: bool { y == true <==> L.mem x l == true } )
= match l with
  | [] -> false
  | a :: q -> (x = a || list_mem x q)

inline_for_extraction
let enum_key (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (s: key { list_mem s (list_map fst e) } )

inline_for_extraction
let make_enum_key (#key #repr: eqtype) (e: enum key repr) (k: key) : Pure (enum_key e)
  (requires (list_mem k (list_map fst e)))
  (ensures (fun k' -> k == (k' <: key)))
= k

inline_for_extraction
let enum_repr (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (r: repr { list_mem r (list_map snd e) } )

let flip (#a #b: Type) (c: (a * b)) : Tot (b * a) = let (ca, cb) = c in (cb, ca)

let rec map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map flip (list_map flip l) == l)
= match l with
  | [] -> ()
  | _ :: q -> map_flip_flip q

let rec map_fst_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map fst (list_map flip l) == list_map snd l)
= match l with
  | [] -> ()
  | _ :: q -> map_fst_flip q

let rec map_snd_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map snd (list_map flip l) == list_map fst l)
= match l with
  | [] -> ()
  | _ :: q -> map_snd_flip q

let rec assoc_mem_snd
  (#a #b: eqtype)
  (l: list (a * b))
  (x: a)
  (y: b)
: Lemma
  (requires (L.assoc x l == Some y))
  (ensures (list_mem y (list_map snd l) == true))
  (decreases l)
= let ((x', y') :: l') = l in
  if x' = x
  then ()
  else assoc_mem_snd l' x y

let rec assoc_flip_elim
  (#a #b: eqtype)
  (l: list (a * b))
  (y: b)
  (x: a)
: Lemma
  (requires (
    L.noRepeats (list_map fst l) /\
    L.noRepeats (list_map snd l) /\
    L.assoc y (list_map flip l) == Some x
  ))
  (ensures (
    L.assoc x l == Some y
  ))
  (decreases l)
= let ((x', y') :: l') = l in
  if y' = y
  then ()
  else begin
    if x' = x
    then begin
      assert (list_mem x' (list_map fst l') == false);
      assoc_mem_snd (list_map flip l') y x;
      map_snd_flip l';
      assert False
    end
    else
      assoc_flip_elim l' y x
  end

let rec assoc_flip_intro
  (#a #b: eqtype)
  (l: list (a * b))
  (y: b)
  (x: a)
: Lemma
  (requires (
    L.noRepeats (list_map fst l) /\
    L.noRepeats (list_map snd l) /\
    L.assoc x l == Some y
  ))
  (ensures (
    L.assoc y (list_map flip l) == Some x
  ))
= map_fst_flip l;
  map_snd_flip l;
  map_flip_flip l;
  assoc_flip_elim (list_map flip l) x y

let enum_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: enum_repr e)
: Pure (enum_key e)
  (requires True)
  (ensures (fun y -> L.assoc y e == Some r))
= map_fst_flip e;
  let e' = list_map #(key * repr) #(repr * key) flip e in
  L.assoc_mem r e';
  let k = Some?.v (L.assoc r e') in
  assoc_flip_elim e r k;
  L.assoc_mem k e;
  (k <: enum_key e)

let parse_enum_key_cond
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr)
: GTot bool
= list_mem r (list_map snd e)

let parse_enum_key_synth
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr { parse_enum_key_cond e r == true } )
: GTot (enum_key e)
= enum_key_of_repr e r

let parse_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: enum key repr)
: Tot (parser (parse_filter_kind k) (enum_key e))
= (p
    `parse_filter`
    parse_enum_key_cond e
  )
  `parse_synth`
  parse_enum_key_synth e

let enum_repr_of_key
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: Pure (enum_repr e)
  (requires True)
  (ensures (fun r -> L.assoc k e == Some r))
= L.assoc_mem k e;
  let r = Some?.v (L.assoc k e) in
  assoc_flip_intro e r k;
  L.assoc_mem r (list_map flip e);
  map_fst_flip e;
  (r <: enum_repr e)

let enum_repr_of_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: enum_repr e)
: Lemma
  (enum_repr_of_key e (enum_key_of_repr e r) == r)
= ()

let enum_key_of_repr_of_key
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: Lemma
  (enum_key_of_repr e (enum_repr_of_key e k) == k)
= assoc_flip_intro e (enum_repr_of_key e k) k

let serialize_enum_key_synth_recip 
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: GTot (r: repr { parse_enum_key_cond e r == true } )
= enum_repr_of_key e k

let serialize_enum_key_synth_inverse
  (#key #repr: eqtype)
  (e: enum key repr)
: Lemma
  (synth_inverse (parse_enum_key_synth e) (serialize_enum_key_synth_recip e))
= Classical.forall_intro (enum_key_of_repr_of_key e)

let serialize_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
: Tot (serializer (parse_enum_key p e))
= serialize_enum_key_synth_inverse e;
  serialize_synth
    (parse_filter p (parse_enum_key_cond e))
    (parse_enum_key_synth e)
    (serialize_filter s (parse_enum_key_cond e))
    (serialize_enum_key_synth_recip e)
    ()

let serialize_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
  (x: enum_key e)
: Lemma
  (serialize (serialize_enum_key p s e) x == serialize s (enum_repr_of_key e x))
= serialize_enum_key_synth_inverse e;
  serialize_synth_eq
    (parse_filter p (parse_enum_key_cond e))
    (parse_enum_key_synth e)
    (serialize_filter s (parse_enum_key_cond e))
    (serialize_enum_key_synth_recip e)
    ()
    x

inline_for_extraction
let unknown_enum_repr (#key #repr: eqtype) (e: enum key repr) : Tot Type =
  (r: repr { list_mem r (list_map snd e) == false } )

type maybe_enum_key (#key #repr: eqtype) (e: enum key repr) =
| Known of (enum_key e)
| Unknown of (unknown_enum_repr e)

let maybe_enum_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr)
: Tot (maybe_enum_key e)
= if list_mem r (list_map snd e)
  then Known (enum_key_of_repr e r)
  else Unknown r

let parse_maybe_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: enum key repr)
: Tot (parser k (maybe_enum_key e))
= p `parse_synth` (maybe_enum_key_of_repr e)

let parse_maybe_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: enum key repr)
  (input: bytes)
: Lemma
  (parse (parse_maybe_enum_key p e) input == (match parse p input with
  | Some (x, consumed) -> Some (maybe_enum_key_of_repr e x, consumed)
  | _ -> None
  ))
= parse_synth_eq p (maybe_enum_key_of_repr e) input

let parse_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: enum key repr)
  (input: bytes)
: Lemma
  (parse (parse_enum_key p e) input == (match parse p input with
  | Some (x, consumed) ->
    begin match maybe_enum_key_of_repr e x with
    | Known k -> Some (k, consumed)
    | _ -> None
    end
  | _ -> None
  ))
= parse_filter_eq p (parse_enum_key_cond e) input;
  parse_synth_eq (p `parse_filter` parse_enum_key_cond e) (parse_enum_key_synth e) input

let repr_of_maybe_enum_key
  (#key #repr: eqtype)
  (e: enum key repr)
  (x: maybe_enum_key e)
: Tot (r: repr { maybe_enum_key_of_repr e r == x } )
= match x with
  | Known k' ->
    enum_key_of_repr_of_key e k' ;
    enum_repr_of_key e k'
  | Unknown r -> r

let serialize_maybe_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
: Tot (serializer (parse_maybe_enum_key p e))
= serialize_synth p (maybe_enum_key_of_repr e) s (repr_of_maybe_enum_key e) ()

let serialize_maybe_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
  (x: maybe_enum_key e)
: Lemma
  (serialize (serialize_maybe_enum_key p s e) x == serialize s (repr_of_maybe_enum_key e x))
= serialize_synth_eq p (maybe_enum_key_of_repr e) s (repr_of_maybe_enum_key e) () x 

let is_total_enum (#key: eqtype) (#repr: eqtype) (l: list (key * repr)) : GTot Type0 =
  forall (k: key) . {:pattern (list_mem k (list_map fst l))} list_mem k (list_map fst l)

let total_enum (key: eqtype) (repr: eqtype) : Tot eqtype =
  (l: enum key repr { is_total_enum l } )

let synth_total_enum_key
  (#key: eqtype)
  (#repr: eqtype)
  (l: total_enum key repr)
  (k: enum_key l)
: Tot key
= let k' : key = k in
  k'

let parse_total_enum_key
  (#k: parser_kind)
  (#key: eqtype)
  (#repr: eqtype)
  (p: parser k repr)
  (l: total_enum key repr)
: Tot (parser (parse_filter_kind k) key)
= parse_enum_key p l `parse_synth` (synth_total_enum_key l)

let synth_total_enum_key_recip
  (#key: eqtype)
  (#repr: eqtype)
  (l: total_enum key repr)
  (k: key)
: Tot (k' : enum_key l { synth_total_enum_key l k' == k } )
= k

let serialize_total_enum_key
  (#k: parser_kind)
  (#key: eqtype)
  (#repr: eqtype)
  (p: parser k repr)
  (s: serializer p)
  (l: total_enum key repr)
: Tot (serializer (parse_total_enum_key p l))
= serialize_synth (parse_enum_key p l) (synth_total_enum_key l) (serialize_enum_key p s l) (synth_total_enum_key_recip l) ()

type maybe_total_enum_key (#key #repr: eqtype) (e: total_enum key repr) =
| TotalKnown of key
| TotalUnknown of (unknown_enum_repr e)

let maybe_total_enum_key_of_repr
  (#key #repr: eqtype)
  (e: total_enum key repr)
  (r: repr)
: Tot (maybe_total_enum_key e)
= if list_mem r (list_map snd e)
  then TotalKnown (enum_key_of_repr e r)
  else TotalUnknown r

let parse_maybe_total_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: total_enum key repr)
: Tot (parser k (maybe_total_enum_key e))
= p `parse_synth` (maybe_total_enum_key_of_repr e)

let repr_of_maybe_total_enum_key
  (#key #repr: eqtype)
  (e: total_enum key repr)
  (k: maybe_total_enum_key e)
: Tot (r: repr { maybe_total_enum_key_of_repr e r == k } )
= match k with
  | TotalKnown k' ->
    enum_key_of_repr_of_key e k' ;
    enum_repr_of_key e k'
  | TotalUnknown r -> r

let serialize_maybe_total_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (s: serializer p)
  (e: total_enum key repr)
: Tot (serializer (parse_maybe_total_enum_key p e))
= serialize_synth p (maybe_total_enum_key_of_repr e) s (repr_of_maybe_total_enum_key e) ()

inline_for_extraction
let maybe_enum_key_of_total
  (#key #repr: eqtype)
  (e: total_enum key repr)
  (k: maybe_total_enum_key e)
: Tot (maybe_enum_key e)
= match k with
  | TotalKnown ek -> Known (ek <: key)
  | TotalUnknown r -> Unknown r

inline_for_extraction
let total_of_maybe_enum_key
  (#key #repr: eqtype)
  (e: total_enum key repr)
  (k: maybe_enum_key e)
: Tot (maybe_total_enum_key e)
= match k with
  | Known ek -> TotalKnown (ek <: key)
  | Unknown r -> TotalUnknown r

let maybe_total_enum_key_of_repr_eq
  (#key #repr: eqtype)
  (e: total_enum key repr)
  (r: repr)
: Lemma
  (maybe_total_enum_key_of_repr e r == total_of_maybe_enum_key e (maybe_enum_key_of_repr e r))
= ()

let parse_maybe_total_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: total_enum key repr)
  (input: bytes)
: Lemma
  (parse (parse_maybe_total_enum_key p e) input == (parse (parse_maybe_enum_key p e `parse_synth` total_of_maybe_enum_key e) input))
= parse_synth_eq p (maybe_total_enum_key_of_repr e) input;
  parse_synth_eq (parse_maybe_enum_key p e) (total_of_maybe_enum_key e) input;
  parse_synth_eq p (maybe_enum_key_of_repr e) input

(* Destructors *)


(* Universal destructor *)

let r_reflexive_prop
  (t: Type)
  (r: (t -> t -> GTot Type0))
: GTot Type0
= forall (x: t) . {:pattern (r x x)} r x x

inline_for_extraction
let r_reflexive_t
  (t: Type)
  (r: (t -> t -> GTot Type0))
: Tot Type
= (x: t) -> Lemma (r x x)

let r_reflexive_t_elim
  (t: Type)
  (r: (t -> t -> GTot Type0))
  (phi: r_reflexive_t t r)
: Lemma
  (r_reflexive_prop t r)
= Classical.forall_intro phi

let r_transitive_prop
  (t: Type)
  (r: (t -> t -> GTot Type0))
: GTot Type0
= forall (x y z: t) . {:pattern (r x y); (r y z)} (r x y /\ r y z) ==> r x z

inline_for_extraction
let r_transitive_t
  (t: Type)
  (r: (t -> t -> GTot Type0))
: Tot Type
= (x: t) -> (y: t) -> (z: t) -> Lemma ((r x y /\ r y z) ==> r x z)

let r_transitive_t_elim
  (t: Type)
  (r: (t -> t -> GTot Type0))
  (phi: r_transitive_t t r)
: Lemma
  (r_transitive_prop t r)
= Classical.forall_intro_3 phi

inline_for_extraction
let if_combinator
  (t: Type)
  (eq: (t -> t -> GTot Type0))
: Tot Type
= (cond: bool) ->
  (sv_true: (cond_true cond -> Tot t)) ->
  (sv_false: (cond_false cond -> Tot t)) ->
  Tot (y: t { eq y (if cond then sv_true () else sv_false ()) } )

inline_for_extraction
let default_if
  (t: Type)
: Tot (if_combinator t (eq2 #t))
= fun
  (cond: bool)
  (s_true: (cond_true cond -> Tot t))
  (s_false: (cond_false cond -> Tot t))
-> (if cond
  then s_true ()
  else s_false ()) <: (y: t { y == (if cond then s_true () else s_false ()) } )

let feq
  (u v: Type)
  (eq: (v -> v -> GTot Type0))
  (f1 f2: (u -> Tot v))
: GTot Type0
= (forall (x: u) . {:pattern (f1 x); (f2 x)} eq (f1 x) (f2 x))

(* #!$% patterns on forall, the following proofs should be trivial and now they aren't *)

let feq_elim
  (u v: Type)
  (eq: (v -> v -> GTot Type0))
  (f1 f2: (u -> Tot v))
  (x: u)
: Lemma
  (requires (feq u v eq f1 f2))
  (ensures (f1 x `eq` f2 x))
= ()

let feq_intro
  (u v: Type)
  (eq: (v -> v -> GTot Type0))
  (f1 f2: (u -> Tot v))
  (phi: (x: u) -> Lemma (f1 x `eq` f2 x))
: Lemma (feq _ _ eq f1 f2)
= Classical.forall_intro phi

let feq_trans
  (u v: Type)
  (eq: (v -> v -> GTot Type0))
: Pure (r_transitive_t _ (feq _ _ eq))
  (requires (r_transitive_prop _ eq))
  (ensures (fun _ -> True))
= let phi
    (f1 f2 f3: (u -> Tot v))
  : Lemma
    (requires (feq _ _ eq f1 f2 /\ feq _ _ eq f2 f3))
    (ensures (feq _ _ eq f1 f3))
  = feq_intro _ _ eq f1 f3 (fun x -> assert (f1 x `eq` f2 x /\ f2 x `eq` f3 x))
  in
  let phi2
    (f1 f2 f3: (u -> Tot v))
  : Lemma
    ((feq _ _ eq f1 f2 /\ feq _ _ eq f2 f3) ==> feq _ _ eq f1 f3)
  = Classical.move_requires (phi f1 f2) f3
  in
  phi2

inline_for_extraction
let fif
  (u v: Type)
  (eq: (v -> v -> GTot Type0))
  (ifc: if_combinator v eq)
: Tot (if_combinator (u -> Tot v) (feq u v eq))
= fun (cond: bool) (s_true: (cond_true cond -> u -> Tot v)) (s_false: (cond_false cond -> u -> Tot v)) (x: u) ->
    ifc
      cond
      (fun h -> s_true () x)
      (fun h -> s_false () x)

inline_for_extraction
let enum_destr_t
  (t: Type)
  (#key #repr: eqtype)  
  (e: enum key repr)
: Tot Type
= (eq: (t -> t -> GTot Type0)) ->
  (ift: if_combinator t eq) ->
  (eq_refl: r_reflexive_t _ eq) ->
  (eq_trans: r_transitive_t _ eq) ->
  (f: ((x: enum_key e) -> Tot t)) ->
  (x: enum_key e) ->
  Tot (y: t { eq y (f x) } )

inline_for_extraction
let enum_tail'
  (#key #repr: eqtype)
  (e: enum key repr)
: Pure (enum key repr)
  (requires True)
  (ensures (fun y -> Cons? e ==> (let (_ :: y') = e in y == y')))
= match e with _ :: y -> y | _ -> []

inline_for_extraction
let enum_tail
  (#key #repr: eqtype)
  (e: enum key repr)
: Tot (enum key repr)
= enum_tail' e

inline_for_extraction
let enum_destr_cons
  (t: Type)
  (#key #repr: eqtype)
  (e: enum key repr)
  (g: enum_destr_t t (enum_tail' e))
: Pure (enum_destr_t t e)
  (requires (Cons? e))
val enum_destr_cons
      (t: Type)
      (#key #repr: eqtype)
      (e: enum key repr)
      (g: enum_destr_t t (enum_tail' e))
    : Pure (enum_destr_t t e) (requires (Cons? e)) (ensures (fun _ -> True))

    t: Type ->
    e: LowParse.Spec.Enum.enum key repr ->
    g: LowParse.Spec.Enum.enum_destr_t t (LowParse.Spec.Enum.enum_tail' e)
  -> Prims.Pure (LowParse.Spec.Enum.enum_destr_t t e)