diff options
author | Josh Chen | 2019-02-28 00:05:23 +0100 |
---|---|---|
committer | Josh Chen | 2019-02-28 00:05:23 +0100 |
commit | 0d4faf23394e2dca1c76bb551f09b642fa5976ac (patch) | |
tree | 414deea207fffbf67d4b44c97c7b3339f248b399 /HoTT_Base.thy | |
parent | 76a009527d42c9939575f429a406a084c48fe653 (diff) |
1. Remove all type inference functionality (feature development moving to another branch).
2. Eq.thy complete.
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1dcf61c..34474d1 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -11,11 +11,20 @@ This file completes the basic logical and functional setup of the HoTT logic. It ********) theory HoTT_Base -imports HoTT_Typing +imports Pure begin +section \<open>Basic setup\<close> + +declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close> + +typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close> + +judgment has_type :: "[t, t] \<Rightarrow> prop" ("(2_ :/ _)") + + section \<open>Universes\<close> typedecl ord \<comment> \<open>Type of meta-numerals\<close> |