diff options
| author | Josh Chen | 2020-07-31 18:10:10 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-31 18:10:10 +0200 |
| commit | 77aa10763429d2ded040071fbf7bee331dd52f5e (patch) | |
| tree | 266abca73311031798c3936c1e44827bda292f25 /spartan/core/typechecking.ML | |
| parent | ff5454812f9e2720bd90c3a5437505644f63b487 (diff) | |
(REF) Tweak attribute names in preparation for new logical introduction rule behavior
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/typechecking.ML | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index a6e1726..b7a7f9b 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -37,8 +37,7 @@ fun put_types typings = foldr1 (op o) (map put_type typings) (* Context tactics for type-checking *) -val debug_typechk = - Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false) +val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false) fun debug_tac ctxt s = if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac @@ -73,9 +72,9 @@ fun check_infer_step facts i (ctxt, st) = map (Simplifier.norm_hhf ctxt) facts (*MAYBE FIXME: Remove `typechk` from this list, and instead perform definitional unfolding to (w?)hnf.*) - @(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>) @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>) - @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) + @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>) @(map #1 (Elim.rules ctxt))) in (resolve_from_net_tac ctxt net) i end else no_tac) |