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/core/congruence.ML | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 spartan/core/congruence.ML

(limited to 'spartan/core/congruence.ML')

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
-- 
cgit v1.2.3