aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--HoTT_Base.thy2
1 files changed, 2 insertions, 0 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 2ad0ac5..69cc1b1 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -14,6 +14,8 @@ begin
section \<open>Basic setup\<close>
+declare[[eta_contract=false]]
+
typedecl t \<comment> \<open>Type of object types and terms\<close>
typedecl ord \<comment> \<open>Type of meta-level numerals\<close>