diff options
| author | Josh Chen | 2018-08-18 21:28:21 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 21:28:21 +0200 |
| commit | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (patch) | |
| tree | 37fa2dacc40261bf37726e23121df0ba5b9af68e /HoTT_Methods.thy | |
| parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) | |
Regrouping type rules
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 316841d..4d2174b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/HoTT_Methods.thy Author: Josh Chen - Date: Jun 2018 Method setup for the HoTT library. Relies heavily on Eisbach. *) @@ -18,7 +17,7 @@ section \<open>Method definitions\<close> subsection \<open>Simple type rule proof search\<close> text " - Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas. + Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas. Can also perform typechecking, and search for elements of a type. " @@ -62,7 +61,7 @@ ML_file "~~/src/Tools/eqsubst.ML" text "Perform basic single-step computations:" -method compute uses lems = (subst lems comp) +method compute uses lems = (subst lems comp | rule lems comp) end |