diff options
author | Josh Chen | 2018-07-12 01:46:30 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-12 01:46:30 +0200 |
commit | 1be12499f63119d9455e2baa917659806732ca7d (patch) | |
tree | b65f13beb0231c6fbac99eac5e980155477c8074 /HoTT_Methods.thy | |
parent | 9723fc3ffc55b22a2a8ec09cbba80f14c40d7991 (diff) |
Unit and Null types. Methods.
Diffstat (limited to '')
-rw-r--r-- | HoTT_Methods.thy | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c314ed4..8a4417d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -49,14 +49,17 @@ method wellformed uses jdgmt declares wellform = subsection \<open>Derivation search\<close> -text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments. +text "Combine \<open>simple\<close>, \<open>wellformed\<close> and the universe hierarchy rules to search for derivations of judgments. \<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments. Definitions passed as \<open>unfolds\<close> are unfolded throughout." method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | - match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> + match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> | + rule Universe_hierarchy | + (rule Universe_cumulative, simple lems: lems) | + (rule Universe_cumulative, match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>) )+ |