val enum_destr_tac (#key #repr: Type) (e: list (key * repr)) : T.Tac unit
let enum_destr_tac
  (#key #repr: Type)
  (e: list (key * repr))
: T.Tac unit
= enum_tac_gen (quote enum_destr_cons_nil') (quote enum_destr_cons') e
val enum_destr_tac (#key #repr: Type) (e: list (key * repr)) : T.Tac unit
let enum_destr_tac (#key #repr: Type) (e: list (key * repr)) : T.Tac unit =
enum_tac_gen (quote enum_destr_cons_nil') (quote enum_destr_cons') e
LowParse.Spec.Tac.Sum.fst.checked
prims.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.Tac.Enum.fst.checked LowParse.Spec.Sum.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked
LowParse.Spec.Tac.Sum.fst
Prims.list FStar.Pervasives.Native.tuple2 LowParse.Spec.Tac.Enum.enum_tac_gen Prims.unit FStar.Reflection.Types.term LowParse.Spec.Enum.enum_destr_cons' LowParse.Spec.Enum.enum_destr_cons_nil'
module LowParse.Spec.Tac.Sum
include LowParse.Spec.Tac.Enum
include LowParse.Spec.Sum

module T = LowParse.TacLib
module U32 = FStar.UInt32


(* Universal destructor *)

noextract
let enum_destr_tac
  (#key #repr: Type)
  (e: list (key * repr))
val enum_destr_tac (#key #repr: Type) (e: list (key * repr)) : T.Tac unit
e: Prims.list (key * repr) -> FStar.Tactics.Effect.Tac Prims.unit