diff options
| author | Josh Chen | 2019-01-31 15:51:24 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-01-31 15:51:24 +0100 |
| commit | 07d312b312c3058551353bcf403a1dc7c7c83311 (patch) | |
| tree | c92ce3160b32a8740c951ca3f64bd0445d42d417 | |
| parent | def15c3748599d5c05cae164653e85ea03da6be6 (diff) | |
Text remarks
| -rw-r--r-- | HoTT_Base.thy | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 99ab5ce..bb47a74 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,7 +2,7 @@ Isabelle/HoTT: Foundational definitions and notation Jan 2019 -This file is the starting point, and contains the base setup and definitions of the object logic. +This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions. Among other things, it defines: * Meta-numerals to index the universe hierarchy, and related axioms. @@ -18,7 +18,7 @@ begin section \<open>Basic setup\<close> -declare[[eta_contract=false]] (* I'm not actually sure this does anything... *) +declare[[eta_contract=false]] (* Does this option actually do anything? *) typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close> typedecl ord \<comment> \<open>Type of meta-numerals\<close> @@ -55,9 +55,13 @@ text \<open> Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination. Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. -@{thm U_cumulative'} is an alternative rule used by the method \<open>cumulativity\<close> in @{file HoTT_Methods.thy}. +@{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}. \<close> +section \<open>Type families\<close> + +abbrev (input) + section \<open>Named theorems\<close> named_theorems comp |