From 8759a6ff0dbe5f0e9dbc28ab2711c54bed7ffa44 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:29:10 +0100
Subject: Decided to keep terms eta-expanded

---
 HoTT_Base.thy | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index aa13815..88cf986 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -18,6 +18,8 @@ begin
 
 section \<open>Terms and typing\<close>
 
+declare[[eta_contract=false]]
+
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
 
 judgment has_type :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
-- 
cgit v1.2.3