val synth_case_synth_case_recip_tac: Prims.unit -> T.Tac unit
let synth_case_synth_case_recip_tac
  ()
: T.Tac unit
= make_sum_synth_case_recip_synth_case_tac ()
val synth_case_synth_case_recip_tac: Prims.unit -> T.Tac unit
let synth_case_synth_case_recip_tac () : T.Tac unit =
make_sum_synth_case_recip_synth_case_tac ()
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.unit LowParse.Spec.Tac.Sum.make_sum_synth_case_recip_synth_case_tac
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))
: T.Tac unit
= enum_tac_gen (quote enum_destr_cons_nil') (quote enum_destr_cons') e

noextract
let make_sum_synth_case_recip_synth_case_tac
  ()
: T.Tac unit
= 
    let x = T.binder_to_term (T.intro ()) in
    T.destruct x;
    T.to_all_goals (fun () ->
      let xeq = T.intros_until_squash () in
      T.norm [delta; iota; zeta; primops];
      T.rewrite xeq;
      T.norm [delta; iota; zeta; primops];
      T.trivial ()
    )

noextract
let make_dsum_synth_case_recip_synth_case_known_tac
  ()
: T.Tac unit
= make_sum_synth_case_recip_synth_case_tac ()

noextract
let make_dsum_synth_case_recip_synth_case_unknown_tac
  ()
: T.Tac unit
= let x = T.binder_to_term (T.intro ()) in
  T.norm [delta; iota; zeta; primops];
  T.trivial ()

noextract
let synth_case_synth_case_recip_tac
  ()
val synth_case_synth_case_recip_tac: Prims.unit -> T.Tac unit
_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit