diff options
| author | Josh Chen | 2020-07-11 15:10:42 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-11 15:10:42 +0200 |
| commit | 861274890a73702aa4c8d74dac8991bdc0e840de (patch) | |
| tree | abfd90e62063436333924e6acf4ddac7960af996 /spartan/core/types.ML | |
| parent | 831f33468f227c0dc96bd31380236f2c77e70c52 (diff) | |
rename file
Diffstat (limited to 'spartan/core/types.ML')
| -rw-r--r-- | spartan/core/types.ML | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/spartan/core/types.ML b/spartan/core/types.ML deleted file mode 100644 index 1eaf60b..0000000 --- a/spartan/core/types.ML +++ /dev/null @@ -1,29 +0,0 @@ -(* Title: types.ML - Author: Joshua Chen - -Type information storage. -*) - -structure Types: sig - -val Data: Proof.context -> thm Item_Net.T -val types: Proof.context -> term -> thm list -val put_type: thm -> Proof.context -> Proof.context -val put_types: thm list -> Proof.context -> Proof.context - -end = 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 -) - -val Data = Data.get o Context.Proof -fun types ctxt tm = Item_Net.retrieve (Data ctxt) tm -fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing)) -fun put_types typings = foldr1 (op o) (map put_type typings) - -end |