From 76deb7ae15fa00b5498ab43db020a0364499251e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 6 Jul 2018 10:48:41 +0200
Subject: Added attributes to type elimination rules, not sure if these will
 actually be needed or useful later. Added [comp] attribute to be used by
 simplification met methods.

---
 HoTT_Base.thy | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index eaebfb0..cfced79 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -12,9 +12,13 @@ begin
 
 section \<open>Setup\<close>
 
-text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments, to be used by proof methods later (see HoTT_Methods.thy)."
+text "Named theorems to be used by proof methods later (see HoTT_Methods.thy).
+
+\<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while
+\<open>comp\<close> declares computation rules used when simplifying function application."
 
 named_theorems wellform
+named_theorems comp
 
 
 section \<open>Metalogical definitions\<close>
@@ -32,8 +36,8 @@ text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> s
 For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it."
 
 consts
-  is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
-  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
+  is_a_type :: "Term \<Rightarrow> prop"           ("(1_ : U)" [0] 1000)
+  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ : _)" [0, 0] 1000)
 
 text "The following fact is used to make explicit the assumption of well-formed contexts."
 
-- 
cgit v1.2.3

