From 0d4faf23394e2dca1c76bb551f09b642fa5976ac Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 Feb 2019 00:05:23 +0100
Subject: 1. Remove all type inference functionality (feature development
 moving to another branch). 2. Eq.thy complete.

---
 HoTT_Base.thy | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'HoTT_Base.thy')

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>
-- 
cgit v1.2.3