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 \Setup\ -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). + +\wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while +\comp\ declares computation rules used when simplifying function application." named_theorems wellform +named_theorems comp section \Metalogical definitions\ @@ -32,8 +36,8 @@ text "We formalize the judgments \a : A\ and \A : U\ s For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it." consts - is_a_type :: "Term \ prop" ("(1_ :/ U)" [0] 1000) - is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) + is_a_type :: "Term \ prop" ("(1_ : U)" [0] 1000) + is_of_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 0] 1000) text "The following fact is used to make explicit the assumption of well-formed contexts." -- cgit v1.2.3