diff options
| author | Josh Chen | 2019-03-03 22:47:03 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-03 22:48:25 +0100 |
| commit | 38dd685f6929d402a32ddfe2d913c7b380b9e935 (patch) | |
| tree | 8456c696707d90816aef0a6a88db98a873a8fde7 /HoTT_Methods.thy | |
| parent | de6672d6682aea2e7df9e71b2325365dd1383507 (diff) | |
Improve automated handling of universes. derive now can automatically handle more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much.
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 27f252b..e45608e 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -64,11 +64,12 @@ section \<open>Derivation search\<close> text \<open> The method @{theory_text derive} combines @{method routine} and @{method compute} to search for derivations of judgments. -It also handles universes using @{method hierarchy} and @{method cumulativity}. +It also handles universes using @{method cumulativity}. +The method @{method hierarchy} has been observed to cause looping in previous versions, and is hence no longer part of @{theory_text derive}. \<close> method derive uses lems declares comp = - (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+ + (routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+ section \<open>Additional method combinators\<close> |