1. Type information context data

2. Small reformulations of rules
3. Bool

1 files changed, 18 insertions, 0 deletions

diff --git a/spartan/core/lib/types.ML b/spartan/core/lib/types.ML
new file mode 100644
index 0000000..b0792fe
--- /dev/null
+++ b/spartan/core/lib/types.ML
@@ -0,0 +1,18 @@
+structure Types
+= struct
+
+structure Data = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o Lib.term_of_typing o Thm.prop_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
+fun put_types typings = foldr1 (op o) (map put_type typings)
+
+fun get_types ctxt tm = Item_Net.retrieve (Data.get (Context.Proof ctxt)) tm
+
+
+end