Reorganize theory structure. In particular, the identity type moves out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

1 files changed, 16 insertions, 0 deletions

diff --git a/spartan/core/congruence.ML b/spartan/core/congruence.ML
new file mode 100644
index 0000000..bb7348c
--- /dev/null
+++ b/spartan/core/congruence.ML
@@ -0,0 +1,16 @@
+signature Sym_Attr_Data =
+sig
+  val name: string
+  val symmetry_rule: thm
+end
+
+functor Sym_Attr (D: Sym_Attr_Data) =
+struct
+  local
+    val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
+  in
+    val attr = Thm.rule_attribute []
+      (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
+    val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
+  end
+end