From 80edbd08e13200d2c080ac281d19948bbbcd92e0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 17:09:54 +0200
Subject: Reorganize theory structure. In particular, the identity type moves
 out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

---
 spartan/lib/elimination.ML | 46 ----------------------------------------------
 1 file changed, 46 deletions(-)
 delete mode 100644 spartan/lib/elimination.ML

(limited to 'spartan/lib/elimination.ML')

diff --git a/spartan/lib/elimination.ML b/spartan/lib/elimination.ML
deleted file mode 100644
index 617f83e..0000000
--- a/spartan/lib/elimination.ML
+++ /dev/null
@@ -1,46 +0,0 @@
-(*  Title:      elimination.ML
-    Author:     Joshua Chen
-
-Type elimination setup.
-*)
-
-structure Elim: sig
-
-val rules: Proof.context -> (thm * indexname list) list
-val lookup_rule: Proof.context -> Termtab.key -> (thm * indexname list) option
-val register_rule: term list -> thm -> Context.generic -> Context.generic
-
-end = struct
-
-(** Context data **)
-
-(* Elimination rule data *)
-
-(*Stores elimination rules together with a list of the indexnames of the
-  variables each rule eliminates. Keyed by head of the type being eliminated.*)
-structure Rules = Generic_Data (
-  type T = (thm * indexname list) Termtab.table
-  val empty = Termtab.empty
-  val extend = I
-  val merge = Termtab.merge (eq_fst Thm.eq_thm_prop)
-)
-
-fun rules ctxt = map (op #2) (Termtab.dest (Rules.get (Context.Proof ctxt)))
-fun lookup_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
-fun register_rule tms rl =
-  let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
-  in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end
-
-
-(* [elims] attribute *)
-val _ = Theory.setup (
-  Attrib.setup \<^binding>\<open>elims\<close>
-    (Scan.repeat Args.term_pattern >>
-      (Thm.declaration_attribute o register_rule))
-    ""
-  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>,
-      fn context => (map #1 (rules (Context.proof_of context))))
-)
-
-
-end
-- 
cgit v1.2.3