aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-08-18 23:57:38 +0200
committerJosh Chen2018-08-18 23:57:38 +0200
commit2498c1512a81a9a73a5a8b6a1a0018ad824df778 (patch)
treed2b92d85d8fcdda39d33f68c81e67f3e432a499f
parent33d4303596ab0cc984f270fcce4623f8b384bda7 (diff)
Distinguish the typing judgment
-rw-r--r--HoTT_Base.thy3
1 files changed, 1 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index a229e83..1110e14 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -23,8 +23,7 @@ text "
For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
"
-consts
- has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000)
+judgment has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000)
section \<open>Universe hierarchy\<close>