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_Base.thy | |
parent | 9723fc3ffc55b22a2a8ec09cbba80f14c40d7991 (diff) |
Unit and Null types. Methods.
Diffstat (limited to '')
-rw-r--r-- | HoTT_Base.thy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 703f1aa..8c45d35 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -54,7 +54,7 @@ and Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans - \<comment> \<open>Lets \<open>standard\<close> automatically solve inequalities.\<close> + \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> text "Universe types:" @@ -64,6 +64,7 @@ where Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" and Universe_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" + \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> section \<open>Type families\<close> |