From 0085798a86a35e2430a97289e894724f688db435 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 23 Jun 2021 16:26:23 +0100
Subject: 1. Put universe level parameters first in automatic term definitions.
 2. Add debugging to typechecker

---
 mltt/core/MLTT.thy | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'mltt/core/MLTT.thy')

diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index cd8ae42..5888a90 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -137,9 +137,6 @@ translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)"
 abbreviation Prod (infixl "\<times>" 60)
   where "A \<times> B \<equiv> \<Sum>_: A. B"
 
-abbreviation "and" (infixl "\<and>" 60)
-  where "A \<and> B \<equiv> A \<times> B"
-
 axiomatization where
   SigF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and
 
-- 
cgit v1.2.3