From 613d8642b1154dde0c026cbdcd96568910198251 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Apr 2020 22:32:06 +0200 Subject: [PATCH] decentralized notation in lambda + Makefile update --- .gitignore | 2 + matita/matita/lib/lambda/Makefile | 60 ++++++--- .../matita/lib/lambda/background/notation.ma | 104 --------------- .../matita/lib/lambda/background/preamble.ma | 21 ++- matita/matita/lib/lambda/background/xoa.ma | 110 ---------------- .../lib/lambda/background/xoa_notation.ma | 122 ------------------ .../lib/lambda/levels/iterated_abstraction.ma | 2 + matita/matita/lib/lambda/levels/term.ma | 7 +- .../notation/functions/abstraction_1.ma | 17 +++ .../notation/functions/abstraction_2.ma | 17 +++ .../functions/annotatedabstraction_2.ma | 17 +++ .../notation/functions/application_2.ma | 17 +++ .../notation/functions/application_3.ma | 17 +++ .../lambda/notation/functions/backward_1.ma | 4 +- .../lambda/notation/functions/backward_3.ma | 4 +- .../lib/lambda/notation/functions/dsubst_3.ma | 22 ++++ .../lambda/notation/functions/forward_1.ma | 4 +- .../lambda/notation/functions/forward_3.ma | 4 +- .../lib/lambda/notation/functions/hocons_2.ma | 17 +++ .../lib/lambda/notation/functions/lift_3.ma | 25 ++++ .../notation/functions/multiplicity_1.ma | 17 +++ .../lib/lambda/notation/functions/nil_0.ma | 18 +++ .../notation/functions/projectdown_1.ma | 17 +++ .../notation/functions/projectsame_2.ma | 17 +++ .../lambda/notation/functions/projectup_2.ma | 17 +++ .../functions/variablereferencebyindex_1.ma | 17 +++ .../functions/variablereferencebyindex_2.ma | 17 +++ .../functions/variablereferencebylevel_2.ma | 17 +++ .../notation/relations/decomposedstd_2.ma | 17 +++ .../lib/lambda/notation/relations/parred_2.ma | 17 +++ .../lambda/notation/relations/parredstar_2.ma | 17 +++ .../lib/lambda/notation/relations/prec_2.ma | 18 +++ .../lib/lambda/notation/relations/seqred_2.ma | 18 +++ .../lib/lambda/notation/relations/seqred_3.ma | 17 +++ .../lambda/notation/relations/seqredstar_2.ma | 17 +++ .../lambda/notation/relations/seqredstar_3.ma | 17 +++ .../lib/lambda/notation/relations/std_3.ma | 17 +++ .../lambda/notation/relations/stdstar_3.ma | 17 +++ .../matita/lib/lambda/notation/xoa/ex_1_2.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_2_2.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_2_3.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_3_1.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_3_2.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_3_3.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_3_4.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_4_1.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_4_2.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/ex_4_3.ma | 26 ++++ .../matita/lib/lambda/notation/xoa/false_0.ma | 18 +++ matita/matita/lib/lambda/notation/xoa/or_3.ma | 22 ++++ .../matita/lib/lambda/notation/xoa/true_0.ma | 18 +++ .../lib/lambda/paths/dst_computation.ma | 6 +- .../paths/labeled_sequential_computation.ma | 2 + .../paths/labeled_sequential_reduction.ma | 4 + .../lambda/paths/labeled_st_computation.ma | 8 +- .../lib/lambda/paths/labeled_st_reduction.ma | 9 +- .../lib/lambda/paths/standard_precedence.ma | 2 + matita/matita/lib/lambda/subterms/boolean.ma | 9 +- .../matita/lib/lambda/subterms/booleanized.ma | 8 +- matita/matita/lib/lambda/subterms/carrier.ma | 8 +- .../subterms/relocating_substitution.ma | 2 + .../matita/lib/lambda/subterms/relocation.ma | 2 + matita/matita/lib/lambda/subterms/subterms.ma | 4 + .../lib/lambda/terms/iterated_abstraction.ma | 2 + .../matita/lib/lambda/terms/multiplicity.ma | 6 +- .../lib/lambda/terms/parallel_computation.ma | 2 + .../lib/lambda/terms/parallel_reduction.ma | 4 + .../lambda/terms/relocating_substitution.ma | 2 + matita/matita/lib/lambda/terms/relocation.ma | 2 + .../lambda/terms/sequential_computation.ma | 2 + .../lib/lambda/terms/sequential_reduction.ma | 2 + matita/matita/lib/lambda/terms/term.ma | 4 + matita/matita/lib/lambda/xoa.conf.xml | 9 +- matita/matita/lib/lambda/xoa/ex_1_2.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_2_2.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_2_3.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_3_1.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_3_2.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_3_3.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_3_4.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_4_1.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_4_2.ma | 28 ++++ matita/matita/lib/lambda/xoa/ex_4_3.ma | 28 ++++ matita/matita/lib/lambda/xoa/or_3.ma | 30 +++++ 84 files changed, 1217 insertions(+), 412 deletions(-) delete mode 100644 matita/matita/lib/lambda/background/notation.ma delete mode 100644 matita/matita/lib/lambda/background/xoa.ma delete mode 100644 matita/matita/lib/lambda/background/xoa_notation.ma create mode 100644 matita/matita/lib/lambda/notation/functions/abstraction_1.ma create mode 100644 matita/matita/lib/lambda/notation/functions/abstraction_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/annotatedabstraction_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/application_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/application_3.ma create mode 100644 matita/matita/lib/lambda/notation/functions/dsubst_3.ma create mode 100644 matita/matita/lib/lambda/notation/functions/hocons_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/lift_3.ma create mode 100644 matita/matita/lib/lambda/notation/functions/multiplicity_1.ma create mode 100644 matita/matita/lib/lambda/notation/functions/nil_0.ma create mode 100644 matita/matita/lib/lambda/notation/functions/projectdown_1.ma create mode 100644 matita/matita/lib/lambda/notation/functions/projectsame_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/projectup_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/variablereferencebyindex_1.ma create mode 100644 matita/matita/lib/lambda/notation/functions/variablereferencebyindex_2.ma create mode 100644 matita/matita/lib/lambda/notation/functions/variablereferencebylevel_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/decomposedstd_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/parred_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/parredstar_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/prec_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/seqred_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/seqred_3.ma create mode 100644 matita/matita/lib/lambda/notation/relations/seqredstar_2.ma create mode 100644 matita/matita/lib/lambda/notation/relations/seqredstar_3.ma create mode 100644 matita/matita/lib/lambda/notation/relations/std_3.ma create mode 100644 matita/matita/lib/lambda/notation/relations/stdstar_3.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_1_2.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_2_2.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_2_3.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_3_1.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_3_2.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_3_3.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_3_4.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_4_1.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_4_2.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/ex_4_3.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/false_0.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/or_3.ma create mode 100644 matita/matita/lib/lambda/notation/xoa/true_0.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_1_2.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_2_2.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_2_3.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_3_1.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_3_2.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_3_3.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_3_4.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_4_1.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_4_2.ma create mode 100644 matita/matita/lib/lambda/xoa/ex_4_3.ma create mode 100644 matita/matita/lib/lambda/xoa/or_3.ma diff --git a/.gitignore b/.gitignore index f8a1df2a7..9f322dc4c 100644 --- a/.gitignore +++ b/.gitignore @@ -77,6 +77,8 @@ helm/www/lambdadelta/xslt/changes.xsl helm/www/lambdadelta/xslt/chc_45.xsl helm/www/lambdadelta/xslt/xhtbl.xsl +matita/matita/lib/lambda/.depend + matita/matita/contribs/lambdadelta/.depend matita/matita/contribs/lambdadelta/bin/nodes matita/matita/contribs/lambdadelta/bin/token diff --git a/matita/matita/lib/lambda/Makefile b/matita/matita/lib/lambda/Makefile index b715eb42a..96ae6448a 100644 --- a/matita/matita/lib/lambda/Makefile +++ b/matita/matita/lib/lambda/Makefile @@ -1,29 +1,53 @@ -H = @ -XOA_DIR = ../../../components/binaries/xoa -XOA = xoa.native -DEP_DIR = ../../../components/binaries/matitadep -DEP = matitadep.native -MAC_DIR = ../../../components/binaries/mac -MAC = mac.native +H := @ -XOA_CONF = xoa.conf.xml -XOA_TARGETS = background/xoa_notation.ma background/xoa.ma +TAGS := all xoa deps top -all: xoa - $(H)../../matitac.opt */*.ma +all: + $(H)../../matitac.opt . # xoa ######################################################################## -xoa: $(XOA_TARGETS) +XOA_DIR := ../../../components/binaries/xoa +XOA := xoa.native +XOA_CONF := xoa.conf.xml +XOA_OPTS := ../../matita.conf.xml $(XOA_CONF) -$(XOA_TARGETS): $(XOA_CONF) +xoa: $(XOA_CONF) @echo " EXEC $(XOA) $(XOA_CONF)" - $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF) + $(H)$(XOA_DIR)/$(XOA) -s $(XOA_OPTS) + +# dep input ################################################################## + +DEP_INPUT := .depend +DEP_DIR := ../../../components/binaries/matitadep +DEP := matitadep.native +DEP_OPTS := + +$(DEP_INPUT): MAS = $(shell find $* -name "*.ma") + +$(DEP_INPUT): LINE = $(MAS:%=%:include \"\".) + +$(DEP_INPUT): REPL = sed -e 's/^\./lambda/' + +$(DEP_INPUT): $(MAS) Makefile + @echo " GREP include" + $(H)grep "include \"" $(MAS) | $(REPL) > $(DEP_INPUT) + $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' | $(REPL) >> $(DEP_INPUT) # dep ######################################################################## -deps: MAS = $(shell find $* -name "*.ma") +deps: $(DEP_INPUT) + @echo " MATITADEP -c" + $(H)$(DEP_DIR)/$(DEP) -c $(DEP_OPTS) $< + +# top ######################################################################## + +top: $(DEP_INPUT) + @echo " MATITADEP -t" + $(H)$(DEP_DIR)/$(DEP) -t $(DEP_OPTS) $< + +############################################################################## + +.PHONY: $(TAGS) -deps: $(DEP_DIR)/$(DEP) - @echo " MATITADEP" - $(H)grep "include \"" $(MAS) | $< +.SUFFIXES: diff --git a/matita/matita/lib/lambda/background/notation.ma b/matita/matita/lib/lambda/background/notation.ma deleted file mode 100644 index fdfffb346..000000000 --- a/matita/matita/lib/lambda/background/notation.ma +++ /dev/null @@ -1,104 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* GENERIC NOTATION *********************************************************) - -(* Note: this should go to core_notation *) -notation "⊥" - non associative with precedence 90 - for @{'false}. - -(* Note: this should go to core_notation *) -notation "⊤" - non associative with precedence 90 - for @{'true}. - -(* Note: this should go to core_notation *) -notation "hvbox(a break ≺ b)" - non associative with precedence 45 - for @{ 'prec $a $b }. - -notation "hvbox( # term 90 i )" - non associative with precedence 46 - for @{ 'VariableReferenceByIndex $i }. - -notation "hvbox( { term 46 b } # break term 90 i )" - non associative with precedence 46 - for @{ 'VariableReferenceByIndex $b $i }. - -notation "hvbox( 𝛌 . term 46 A )" - non associative with precedence 46 - for @{ 'Abstraction $A }. - -notation "hvbox( { term 46 b } 𝛌 . break term 46 T)" - non associative with precedence 46 - for @{ 'Abstraction $b $T }. - -notation "hvbox( 𝛌 term 46 d . break term 46 A )" - non associative with precedence 46 - for @{ 'AnnotatedAbstraction $d $A }. - -notation "hvbox( @ term 46 C . break term 46 A )" - non associative with precedence 46 - for @{ 'Application $C $A }. - -notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )" - non associative with precedence 46 - for @{ 'Application $b $V $T }. - -notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Lift $h $d $M }. - -notation > "hvbox( ↑ [ term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Lift $h 0 $M }. - -notation > "hvbox( ↑ term 46 M )" - non associative with precedence 46 - for @{ 'Lift 1 0 $M }. - -(* Note: the notation with "/" does not work *) -notation "hvbox( [ term 46 d break ↙ term 46 N ] break term 46 M )" - non associative with precedence 46 - for @{ 'DSubst $N $d $M }. - -notation > "hvbox( [ ↙ term 46 N ] break term 46 M )" - non associative with precedence 46 - for @{ 'DSubst $N 0 $M }. - -(* Note: we do not use → since it is reserved by CIC *) -notation "hvbox( M break ↦ term 46 N )" - non associative with precedence 45 - for @{ 'SeqRed $M $N }. - -notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" - non associative with precedence 45 - for @{ 'SeqRed $M $p $N }. - -notation "hvbox( M break ↦* term 46 N )" - non associative with precedence 45 - for @{ 'SeqRedStar $M $N }. - -notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" - non associative with precedence 45 - for @{ 'SeqRedStar $M $s $N }. - -notation "hvbox( M break ⤇ term 46 N )" - non associative with precedence 45 - for @{ 'ParRed $M $N }. - -notation "hvbox( M break ⤇* term 46 N )" - non associative with precedence 45 - for @{ 'ParRedStar $M $N }. diff --git a/matita/matita/lib/lambda/background/preamble.ma b/matita/matita/lib/lambda/background/preamble.ma index 6a087e3aa..dd5b0d643 100644 --- a/matita/matita/lib/lambda/background/preamble.ma +++ b/matita/matita/lib/lambda/background/preamble.ma @@ -16,9 +16,15 @@ include "basics/star1.ma". include "basics/lists/lstar.ma". include "arithmetics/exp.ma". -include "lambda/background/xoa_notation.ma". -include "lambda/background/xoa.ma". -include "lambda/background/notation.ma". +include "lambda/notation/xoa/false_0.ma". +include "lambda/notation/xoa/true_0.ma". +include "lambda/xoa/or_3.ma". +include "lambda/xoa/ex_1_2.ma". +include "lambda/xoa/ex_3_2.ma". +include "lambda/xoa/ex_3_3.ma". + +include "lambda/notation/functions/nil_0.ma". +include "lambda/notation/functions/hocons_2.ma". (* logic *) @@ -82,11 +88,6 @@ qed. (* lists *) -(* Note: notation for nil not involving brackets *) -notation > "◊" - non associative with precedence 90 - for @{'nil}. - lemma list_inv: ∀A. ∀l:list A. ◊ = l ∨ ∃∃a0,l0. a0 :: l0 = l. #A * /2 width=1/ /3 width=3/ qed-. @@ -96,10 +97,6 @@ definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a. interpretation "map_cons" 'ho_cons a l = (map_cons ? a l). -notation "hvbox(a ::: break l)" - right associative with precedence 47 - for @{'ho_cons $a $l}. - lemma map_cons_inv_nil: ∀A,a,l1. map_cons A a l1 = ◊ → ◊ = l1. #A #a * // normalize #a1 #l1 #H destruct qed-. diff --git a/matita/matita/lib/lambda/background/xoa.ma b/matita/matita/lib/lambda/background/xoa.ma deleted file mode 100644 index 96a1fb95c..000000000 --- a/matita/matita/lib/lambda/background/xoa.ma +++ /dev/null @@ -1,110 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was generated by xoa.native: do not edit *********************) - -include "basics/pts.ma". - -include "lambda/background/xoa_notation.ma". - -(* multiple existental quantifier (1, 2) *) - -inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ - | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? -. - -interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). - -(* multiple existental quantifier (2, 2) *) - -inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ - | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? -. - -interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). - -(* multiple existental quantifier (2, 3) *) - -inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ - | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). - -(* multiple existental quantifier (3, 1) *) - -inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ - | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). - -(* multiple existental quantifier (3, 2) *) - -inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ - | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). - -(* multiple existental quantifier (3, 3) *) - -inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ - | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). - -(* multiple existental quantifier (3, 4) *) - -inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ - | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). - -(* multiple existental quantifier (4, 1) *) - -inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ - | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 2) *) - -inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ - | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 3) *) - -inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ - | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). - -(* multiple disjunction connective (3) *) - -inductive or3 (P0,P1,P2:Prop) : Prop ≝ - | or3_intro0: P0 → or3 ? ? ? - | or3_intro1: P1 → or3 ? ? ? - | or3_intro2: P2 → or3 ? ? ? -. - -interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). - diff --git a/matita/matita/lib/lambda/background/xoa_notation.ma b/matita/matita/lib/lambda/background/xoa_notation.ma deleted file mode 100644 index 240c1dd5d..000000000 --- a/matita/matita/lib/lambda/background/xoa_notation.ma +++ /dev/null @@ -1,122 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was generated by xoa.native: do not edit *********************) - -(* multiple existental quantifier (1, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. - -(* multiple existental quantifier (2, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. - -(* multiple existental quantifier (2, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. - -(* multiple existental quantifier (3, 1) *) - -notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }. - -notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. - -(* multiple existental quantifier (3, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. - -(* multiple existental quantifier (3, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. - -(* multiple existental quantifier (3, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. - -(* multiple existental quantifier (4, 1) *) - -notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }. - -notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. - -(* multiple existental quantifier (4, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. - -(* multiple existental quantifier (4, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. - -(* multiple disjunction connective (3) *) - -notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" - non associative with precedence 30 - for @{ 'Or $P0 $P1 $P2 }. - diff --git a/matita/matita/lib/lambda/levels/iterated_abstraction.ma b/matita/matita/lib/lambda/levels/iterated_abstraction.ma index c2ad35be7..c9b634987 100644 --- a/matita/matita/lib/lambda/levels/iterated_abstraction.ma +++ b/matita/matita/lib/lambda/levels/iterated_abstraction.ma @@ -14,6 +14,8 @@ include "lambda/levels/term.ma". +include "lambda/notation/functions/annotatedabstraction_2.ma". + (* ITERATED ABSTRACTION *****************************************************) definition labst: nat → lterm → lterm ≝ λh,M. match M with diff --git a/matita/matita/lib/lambda/levels/term.ma b/matita/matita/lib/lambda/levels/term.ma index 593e2b648..d7fd7f32b 100644 --- a/matita/matita/lib/lambda/levels/term.ma +++ b/matita/matita/lib/lambda/levels/term.ma @@ -14,6 +14,9 @@ include "lambda/background/preamble.ma". +include "lambda/notation/functions/variablereferencebylevel_2.ma". +include "lambda/notation/functions/application_3.ma". + (* PER LEVEL TERM STRUCTURE *************************************************) (* Policy: term metavariables : A, B, C, D, M, N @@ -31,7 +34,3 @@ interpretation "stratified term construction (variable reference by level)" interpretation "stratified term construction (application)" 'Application i C A = (LAppl i C A). - -notation "hvbox( { term 46 b } § break term 90 d )" - non associative with precedence 46 - for @{ 'VariableReferenceByLevel $b $d }. diff --git a/matita/matita/lib/lambda/notation/functions/abstraction_1.ma b/matita/matita/lib/lambda/notation/functions/abstraction_1.ma new file mode 100644 index 000000000..410c6613f --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/abstraction_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( 𝛌 . term 46 A )" + non associative with precedence 46 + for @{ 'Abstraction $A }. diff --git a/matita/matita/lib/lambda/notation/functions/abstraction_2.ma b/matita/matita/lib/lambda/notation/functions/abstraction_2.ma new file mode 100644 index 000000000..bc04d2120 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/abstraction_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } 𝛌 . break term 46 T)" + non associative with precedence 46 + for @{ 'Abstraction $b $T }. diff --git a/matita/matita/lib/lambda/notation/functions/annotatedabstraction_2.ma b/matita/matita/lib/lambda/notation/functions/annotatedabstraction_2.ma new file mode 100644 index 000000000..ae7579b84 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/annotatedabstraction_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( 𝛌 term 46 d . break term 46 A )" + non associative with precedence 46 + for @{ 'AnnotatedAbstraction $d $A }. diff --git a/matita/matita/lib/lambda/notation/functions/application_2.ma b/matita/matita/lib/lambda/notation/functions/application_2.ma new file mode 100644 index 000000000..9be610f3e --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/application_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( @ term 46 C . break term 46 A )" + non associative with precedence 46 + for @{ 'Application $C $A }. diff --git a/matita/matita/lib/lambda/notation/functions/application_3.ma b/matita/matita/lib/lambda/notation/functions/application_3.ma new file mode 100644 index 000000000..fbf6e508e --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/application_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )" + non associative with precedence 46 + for @{ 'Application $b $V $T }. diff --git a/matita/matita/lib/lambda/notation/functions/backward_1.ma b/matita/matita/lib/lambda/notation/functions/backward_1.ma index 08ee2b3cd..37fdc2c53 100644 --- a/matita/matita/lib/lambda/notation/functions/backward_1.ma +++ b/matita/matita/lib/lambda/notation/functions/backward_1.ma @@ -13,5 +13,5 @@ (**************************************************************************) notation "hvbox( ⇓ term 46 M )" - non associative with precedence 46 - for @{ 'Backward $M }. + non associative with precedence 46 + for @{ 'Backward $M }. diff --git a/matita/matita/lib/lambda/notation/functions/backward_3.ma b/matita/matita/lib/lambda/notation/functions/backward_3.ma index bfdbfb8a6..a62cc2c04 100644 --- a/matita/matita/lib/lambda/notation/functions/backward_3.ma +++ b/matita/matita/lib/lambda/notation/functions/backward_3.ma @@ -13,5 +13,5 @@ (**************************************************************************) notation "hvbox( ⇓ [ term 46 d , break term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Backward $h $d $M }. + non associative with precedence 46 + for @{ 'Backward $h $d $M }. diff --git a/matita/matita/lib/lambda/notation/functions/dsubst_3.ma b/matita/matita/lib/lambda/notation/functions/dsubst_3.ma new file mode 100644 index 000000000..b9dbf29bc --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/dsubst_3.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: the notation with "/" does not work *) +notation "hvbox( [ term 46 d break ↙ term 46 N ] break term 46 M )" + non associative with precedence 46 + for @{ 'DSubst $N $d $M }. + +notation > "hvbox( [ ↙ term 46 N ] break term 46 M )" + non associative with precedence 46 + for @{ 'DSubst $N 0 $M }. diff --git a/matita/matita/lib/lambda/notation/functions/forward_1.ma b/matita/matita/lib/lambda/notation/functions/forward_1.ma index 32abbf60d..b58876dc6 100644 --- a/matita/matita/lib/lambda/notation/functions/forward_1.ma +++ b/matita/matita/lib/lambda/notation/functions/forward_1.ma @@ -13,5 +13,5 @@ (**************************************************************************) notation "hvbox( ⇑ term 46 M )" - non associative with precedence 46 - for @{ 'Forward $M }. + non associative with precedence 46 + for @{ 'Forward $M }. diff --git a/matita/matita/lib/lambda/notation/functions/forward_3.ma b/matita/matita/lib/lambda/notation/functions/forward_3.ma index ba48d17eb..d91a25f21 100644 --- a/matita/matita/lib/lambda/notation/functions/forward_3.ma +++ b/matita/matita/lib/lambda/notation/functions/forward_3.ma @@ -13,5 +13,5 @@ (**************************************************************************) notation "hvbox( ⇑ [ term 46 d, break term 46 h ] break term 46 M )" - non associative with precedence 46 - for @{ 'Forward $h $d $M }. + non associative with precedence 46 + for @{ 'Forward $h $d $M }. diff --git a/matita/matita/lib/lambda/notation/functions/hocons_2.ma b/matita/matita/lib/lambda/notation/functions/hocons_2.ma new file mode 100644 index 000000000..b12c256d7 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/hocons_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox(a ::: break l)" + right associative with precedence 47 + for @{'ho_cons $a $l}. diff --git a/matita/matita/lib/lambda/notation/functions/lift_3.ma b/matita/matita/lib/lambda/notation/functions/lift_3.ma new file mode 100644 index 000000000..307d5945f --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/lift_3.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Lift $h $d $M }. + +notation > "hvbox( ↑ [ term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Lift $h 0 $M }. + +notation > "hvbox( ↑ term 46 M )" + non associative with precedence 46 + for @{ 'Lift 1 0 $M }. diff --git a/matita/matita/lib/lambda/notation/functions/multiplicity_1.ma b/matita/matita/lib/lambda/notation/functions/multiplicity_1.ma new file mode 100644 index 000000000..6ab279e6f --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/multiplicity_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( ♯{ term 46 M } )" + non associative with precedence 90 + for @{ 'Multiplicity $M }. diff --git a/matita/matita/lib/lambda/notation/functions/nil_0.ma b/matita/matita/lib/lambda/notation/functions/nil_0.ma new file mode 100644 index 000000000..9df2a46db --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/nil_0.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: notation for nil not involving brackets *) +notation > "◊" + non associative with precedence 90 + for @{'nil}. diff --git a/matita/matita/lib/lambda/notation/functions/projectdown_1.ma b/matita/matita/lib/lambda/notation/functions/projectdown_1.ma new file mode 100644 index 000000000..d771417bd --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/projectdown_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox(⇓ term 46 F)" + non associative with precedence 46 + for @{ 'ProjectDown $F }. diff --git a/matita/matita/lib/lambda/notation/functions/projectsame_2.ma b/matita/matita/lib/lambda/notation/functions/projectsame_2.ma new file mode 100644 index 000000000..0404bed17 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/projectsame_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } ⇕ break term 46 F)" + non associative with precedence 46 + for @{ 'ProjectSame $b $F }. diff --git a/matita/matita/lib/lambda/notation/functions/projectup_2.ma b/matita/matita/lib/lambda/notation/functions/projectup_2.ma new file mode 100644 index 000000000..98ddfb765 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/projectup_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } ⇑ break term 46 M)" + non associative with precedence 46 + for @{ 'ProjectUp $b $M }. diff --git a/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_1.ma b/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_1.ma new file mode 100644 index 000000000..e4b15ed5e --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( # term 90 i )" + non associative with precedence 46 + for @{ 'VariableReferenceByIndex $i }. diff --git a/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_2.ma b/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_2.ma new file mode 100644 index 000000000..6295418ce --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/variablereferencebyindex_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } # break term 90 i )" + non associative with precedence 46 + for @{ 'VariableReferenceByIndex $b $i }. diff --git a/matita/matita/lib/lambda/notation/functions/variablereferencebylevel_2.ma b/matita/matita/lib/lambda/notation/functions/variablereferencebylevel_2.ma new file mode 100644 index 000000000..bdbb5358c --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/variablereferencebylevel_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( { term 46 b } § break term 90 d )" + non associative with precedence 46 + for @{ 'VariableReferenceByLevel $b $d }. diff --git a/matita/matita/lib/lambda/notation/relations/decomposedstd_2.ma b/matita/matita/lib/lambda/notation/relations/decomposedstd_2.ma new file mode 100644 index 000000000..b55106fbb --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/decomposedstd_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ⓢ↦* term 46 N )" + non associative with precedence 45 + for @{ 'DecomposedStd $M $N }. diff --git a/matita/matita/lib/lambda/notation/relations/parred_2.ma b/matita/matita/lib/lambda/notation/relations/parred_2.ma new file mode 100644 index 000000000..cb9139d6e --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/parred_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ⤇ term 46 N )" + non associative with precedence 45 + for @{ 'ParRed $M $N }. diff --git a/matita/matita/lib/lambda/notation/relations/parredstar_2.ma b/matita/matita/lib/lambda/notation/relations/parredstar_2.ma new file mode 100644 index 000000000..11443dee1 --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/parredstar_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ⤇* term 46 N )" + non associative with precedence 45 + for @{ 'ParRedStar $M $N }. diff --git a/matita/matita/lib/lambda/notation/relations/prec_2.ma b/matita/matita/lib/lambda/notation/relations/prec_2.ma new file mode 100644 index 000000000..528e170cf --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/prec_2.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: this should go to core_notation *) +notation "hvbox(a break ≺ b)" + non associative with precedence 45 + for @{ 'prec $a $b }. diff --git a/matita/matita/lib/lambda/notation/relations/seqred_2.ma b/matita/matita/lib/lambda/notation/relations/seqred_2.ma new file mode 100644 index 000000000..4edfaf70d --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/seqred_2.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: we do not use → since it is reserved by CIC *) +notation "hvbox( M break ↦ term 46 N )" + non associative with precedence 45 + for @{ 'SeqRed $M $N }. diff --git a/matita/matita/lib/lambda/notation/relations/seqred_3.ma b/matita/matita/lib/lambda/notation/relations/seqred_3.ma new file mode 100644 index 000000000..deb440e0a --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/seqred_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" + non associative with precedence 45 + for @{ 'SeqRed $M $p $N }. diff --git a/matita/matita/lib/lambda/notation/relations/seqredstar_2.ma b/matita/matita/lib/lambda/notation/relations/seqredstar_2.ma new file mode 100644 index 000000000..352aaf3b8 --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/seqredstar_2.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ↦* term 46 N )" + non associative with precedence 45 + for @{ 'SeqRedStar $M $N }. diff --git a/matita/matita/lib/lambda/notation/relations/seqredstar_3.ma b/matita/matita/lib/lambda/notation/relations/seqredstar_3.ma new file mode 100644 index 000000000..efc27d767 --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/seqredstar_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" + non associative with precedence 45 + for @{ 'SeqRedStar $M $s $N }. diff --git a/matita/matita/lib/lambda/notation/relations/std_3.ma b/matita/matita/lib/lambda/notation/relations/std_3.ma new file mode 100644 index 000000000..57c7cb672 --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/std_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )" + non associative with precedence 45 + for @{ 'Std $F $p $G }. diff --git a/matita/matita/lib/lambda/notation/relations/stdstar_3.ma b/matita/matita/lib/lambda/notation/relations/stdstar_3.ma new file mode 100644 index 000000000..6195c501a --- /dev/null +++ b/matita/matita/lib/lambda/notation/relations/stdstar_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )" + non associative with precedence 45 + for @{ 'StdStar $F $p $G }. diff --git a/matita/matita/lib/lambda/notation/xoa/ex_1_2.ma b/matita/matita/lib/lambda/notation/xoa/ex_1_2.ma new file mode 100644 index 000000000..77c7366a6 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_1_2.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (1, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_2_2.ma b/matita/matita/lib/lambda/notation/xoa/ex_2_2.ma new file mode 100644 index 000000000..ccef16288 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_2_2.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (2, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_2_3.ma b/matita/matita/lib/lambda/notation/xoa/ex_2_3.ma new file mode 100644 index 000000000..5e0dba550 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_2_3.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (2, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_3_1.ma b/matita/matita/lib/lambda/notation/xoa/ex_3_1.ma new file mode 100644 index 000000000..f5c367157 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_3_1.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (3, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_3_2.ma b/matita/matita/lib/lambda/notation/xoa/ex_3_2.ma new file mode 100644 index 000000000..8ca34d307 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_3_2.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (3, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_3_3.ma b/matita/matita/lib/lambda/notation/xoa/ex_3_3.ma new file mode 100644 index 000000000..6287d1a4e --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_3_3.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (3, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_3_4.ma b/matita/matita/lib/lambda/notation/xoa/ex_3_4.ma new file mode 100644 index 000000000..5f34348e3 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_3_4.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (3, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_4_1.ma b/matita/matita/lib/lambda/notation/xoa/ex_4_1.ma new file mode 100644 index 000000000..75ac29f16 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_4_1.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (4, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_4_2.ma b/matita/matita/lib/lambda/notation/xoa/ex_4_2.ma new file mode 100644 index 000000000..e8a6e9650 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_4_2.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (4, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/ex_4_3.ma b/matita/matita/lib/lambda/notation/xoa/ex_4_3.ma new file mode 100644 index 000000000..2d52220e2 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/ex_4_3.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (4, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. + diff --git a/matita/matita/lib/lambda/notation/xoa/false_0.ma b/matita/matita/lib/lambda/notation/xoa/false_0.ma new file mode 100644 index 000000000..09b27fb1d --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/false_0.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: this should go to core_notation *) +notation "⊥" + non associative with precedence 90 + for @{'false}. diff --git a/matita/matita/lib/lambda/notation/xoa/or_3.ma b/matita/matita/lib/lambda/notation/xoa/or_3.ma new file mode 100644 index 000000000..3f8265443 --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/or_3.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple disjunction connective (3) *) + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 }. + diff --git a/matita/matita/lib/lambda/notation/xoa/true_0.ma b/matita/matita/lib/lambda/notation/xoa/true_0.ma new file mode 100644 index 000000000..e7a5a0dbf --- /dev/null +++ b/matita/matita/lib/lambda/notation/xoa/true_0.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* Note: this should go to core_notation *) +notation "⊤" + non associative with precedence 90 + for @{'true}. diff --git a/matita/matita/lib/lambda/paths/dst_computation.ma b/matita/matita/lib/lambda/paths/dst_computation.ma index 85874e21c..a9cc98f09 100644 --- a/matita/matita/lib/lambda/paths/dst_computation.ma +++ b/matita/matita/lib/lambda/paths/dst_computation.ma @@ -15,6 +15,8 @@ include "lambda/paths/standard_trace.ma". include "lambda/paths/labeled_sequential_computation.ma". +include "lambda/notation/relations/decomposedstd_2.ma". + (* DECOMPOSED STANDARD COMPUTATION ***********************************************) (* Note: this is the "standard" computation of: @@ -29,10 +31,6 @@ inductive dst: relation term ≝ interpretation "decomposed standard computation" 'DecomposedStd M N = (dst M N). -notation "hvbox( M break ⓢ↦* term 46 N )" - non associative with precedence 45 - for @{ 'DecomposedStd $M $N }. - lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N → ∃∃s. is_whd s & M ↦*[s] #j. #M #N * -M -N diff --git a/matita/matita/lib/lambda/paths/labeled_sequential_computation.ma b/matita/matita/lib/lambda/paths/labeled_sequential_computation.ma index db94f26ba..a4a387ca6 100644 --- a/matita/matita/lib/lambda/paths/labeled_sequential_computation.ma +++ b/matita/matita/lib/lambda/paths/labeled_sequential_computation.ma @@ -16,6 +16,8 @@ include "lambda/terms/labeled_sequential_computation.ma". include "lambda/paths/trace.ma". include "lambda/paths/labeled_sequential_reduction.ma". +include "lambda/notation/relations/seqredstar_3.ma". + (* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) (* Note: lstar shuld be replaced by l_sreds *) diff --git a/matita/matita/lib/lambda/paths/labeled_sequential_reduction.ma b/matita/matita/lib/lambda/paths/labeled_sequential_reduction.ma index 8e9d693b6..5f0123e91 100644 --- a/matita/matita/lib/lambda/paths/labeled_sequential_reduction.ma +++ b/matita/matita/lib/lambda/paths/labeled_sequential_reduction.ma @@ -15,6 +15,10 @@ include "lambda/paths/path.ma". include "lambda/terms/sequential_reduction.ma". +include "lambda/notation/relations/seqred_3.ma". + +include "lambda/xoa/ex_2_2.ma". + (* PATH-LABELED SEQUENTIAL REDUCTION (SINGLE STEP) **************************) inductive pl_sred: path → relation term ≝ diff --git a/matita/matita/lib/lambda/paths/labeled_st_computation.ma b/matita/matita/lib/lambda/paths/labeled_st_computation.ma index a9c19fbb1..a72dae7b9 100644 --- a/matita/matita/lib/lambda/paths/labeled_st_computation.ma +++ b/matita/matita/lib/lambda/paths/labeled_st_computation.ma @@ -16,6 +16,10 @@ include "lambda/paths/standard_trace.ma". include "lambda/paths/labeled_sequential_computation.ma". include "lambda/paths/labeled_st_reduction.ma". +include "lambda/notation/relations/stdstar_3.ma". + +include "lambda/xoa/ex_2_3.ma". + (* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************) (* Note: lstar shuld be replaced by l_sreds *) @@ -24,10 +28,6 @@ definition pl_sts: trace → relation subterms ≝ lstar … pl_st. interpretation "path-labeled standard reduction" 'StdStar F p G = (pl_sts p F G). -notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )" - non associative with precedence 45 - for @{ 'StdStar $F $p $G }. - lemma pl_sts_fwd_pl_sreds: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ⇓F1 ↦*[s] ⇓F2. #s #F1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 // #p #s #F #F2 #_ #HF2 #IHF1 diff --git a/matita/matita/lib/lambda/paths/labeled_st_reduction.ma b/matita/matita/lib/lambda/paths/labeled_st_reduction.ma index 7e8c1578c..60e2c28f8 100644 --- a/matita/matita/lib/lambda/paths/labeled_st_reduction.ma +++ b/matita/matita/lib/lambda/paths/labeled_st_reduction.ma @@ -16,6 +16,11 @@ include "lambda/subterms/booleanized.ma". include "lambda/paths/labeled_sequential_reduction.ma". include "lambda/paths/standard_order.ma". +include "lambda/notation/relations/std_3.ma". + +include "lambda/xoa/ex_4_1.ma". +include "lambda/xoa/ex_3_4.ma". + (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************) (* Note: this is standard reduction on marked redexes, @@ -31,10 +36,6 @@ inductive pl_st: path → relation subterms ≝ interpretation "path-labeled standard reduction" 'Std F p G = (pl_st p F G). -notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )" - non associative with precedence 45 - for @{ 'Std $F $p $G }. - lemma pl_st_fwd_pl_sred: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ⇓F1 ↦[p] ⇓F2. #p #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/ qed-. diff --git a/matita/matita/lib/lambda/paths/standard_precedence.ma b/matita/matita/lib/lambda/paths/standard_precedence.ma index cd61cb223..4a66c5e6e 100644 --- a/matita/matita/lib/lambda/paths/standard_precedence.ma +++ b/matita/matita/lib/lambda/paths/standard_precedence.ma @@ -14,6 +14,8 @@ include "lambda/paths/path.ma". +include "lambda/notation/relations/prec_2.ma". + (* STANDARD PRECEDENCE ******************************************************) (* Note: standard precedence relation on paths: p ≺ q diff --git a/matita/matita/lib/lambda/subterms/boolean.ma b/matita/matita/lib/lambda/subterms/boolean.ma index 66447a3bb..566bfb0a3 100644 --- a/matita/matita/lib/lambda/subterms/boolean.ma +++ b/matita/matita/lib/lambda/subterms/boolean.ma @@ -14,6 +14,11 @@ include "lambda/subterms/carrier.ma". +include "lambda/notation/functions/projectup_2.ma". + +include "lambda/xoa/ex_3_1.ma". +include "lambda/xoa/ex_4_2.ma". + (* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************) let rec boolean b M on M ≝ match M with @@ -25,10 +30,6 @@ let rec boolean b M on M ≝ match M with interpretation "boolean subset (subterms)" 'ProjectUp b M = (boolean b M). -notation "hvbox( { term 46 b } ⇑ break term 46 M)" - non associative with precedence 46 - for @{ 'ProjectUp $b $M }. - lemma boolean_inv_vref: ∀j,c,b,M. {b}⇑ M = {c}#j → b = c ∧ M = #j. #j #c #b * normalize [ #i #H destruct /2 width=1/ diff --git a/matita/matita/lib/lambda/subterms/booleanized.ma b/matita/matita/lib/lambda/subterms/booleanized.ma index d247ee73f..cc6f1e980 100644 --- a/matita/matita/lib/lambda/subterms/booleanized.ma +++ b/matita/matita/lib/lambda/subterms/booleanized.ma @@ -14,6 +14,10 @@ include "lambda/subterms/boolean.ma". +include "lambda/notation/functions/projectsame_2.ma". + +include "lambda/xoa/ex_4_3.ma". + (* BOOLEANIZED SUBSET (EMPTY OR FULL) ***************************************) definition booleanized: bool → subterms → subterms ≝ @@ -22,10 +26,6 @@ definition booleanized: bool → subterms → subterms ≝ interpretation "booleanized (subterms)" 'ProjectSame b F = (booleanized b F). -notation "hvbox( { term 46 b } ⇕ break term 46 F)" - non associative with precedence 46 - for @{ 'ProjectSame $b $F }. - lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j → ∃∃b1. b = c & F = {b1}#j. #j #c #b #F #H diff --git a/matita/matita/lib/lambda/subterms/carrier.ma b/matita/matita/lib/lambda/subterms/carrier.ma index a15e11180..3f4c04991 100644 --- a/matita/matita/lib/lambda/subterms/carrier.ma +++ b/matita/matita/lib/lambda/subterms/carrier.ma @@ -15,6 +15,10 @@ include "lambda/terms/relocating_substitution.ma". include "lambda/subterms/relocating_substitution.ma". +include "lambda/notation/functions/projectdown_1.ma". + +include "lambda/xoa/ex_2_2.ma". + (* CARRIER (UNDERLYING TERM) ************************************************) let rec carrier F on F ≝ match F with @@ -26,10 +30,6 @@ let rec carrier F on F ≝ match F with interpretation "carrier (subterms)" 'ProjectDown F = (carrier F). -notation "hvbox(⇓ term 46 F)" - non associative with precedence 46 - for @{ 'ProjectDown $F }. - lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j. #j * normalize [ #b #i #H destruct /2 width=2/ diff --git a/matita/matita/lib/lambda/subterms/relocating_substitution.ma b/matita/matita/lib/lambda/subterms/relocating_substitution.ma index 6d7fad314..9f803e74c 100644 --- a/matita/matita/lib/lambda/subterms/relocating_substitution.ma +++ b/matita/matita/lib/lambda/subterms/relocating_substitution.ma @@ -14,6 +14,8 @@ include "lambda/subterms/relocation.ma". +include "lambda/notation/functions/dsubst_3.ma". + (* RELOCATING SUBSTITUTION **************************************************) (* Policy: depth (level) metavariables: d, e (as for lift) *) diff --git a/matita/matita/lib/lambda/subterms/relocation.ma b/matita/matita/lib/lambda/subterms/relocation.ma index 99c8ded5a..086e8223a 100644 --- a/matita/matita/lib/lambda/subterms/relocation.ma +++ b/matita/matita/lib/lambda/subterms/relocation.ma @@ -14,6 +14,8 @@ include "lambda/subterms/subterms.ma". +include "lambda/notation/functions/lift_3.ma". + (* RELOCATION FOR SUBTERMS **************************************************) let rec slift h d E on E ≝ match E with diff --git a/matita/matita/lib/lambda/subterms/subterms.ma b/matita/matita/lib/lambda/subterms/subterms.ma index c4ec383b5..acfcde6a4 100644 --- a/matita/matita/lib/lambda/subterms/subterms.ma +++ b/matita/matita/lib/lambda/subterms/subterms.ma @@ -14,6 +14,10 @@ include "lambda/background/preamble.ma". +include "lambda/notation/functions/variablereferencebyindex_2.ma". +include "lambda/notation/functions/abstraction_2.ma". +include "lambda/notation/functions/application_3.ma". + (* SUBSETS OF SUBTERMS ******************************************************) (* Policy: boolean marks metavariables: b,c diff --git a/matita/matita/lib/lambda/terms/iterated_abstraction.ma b/matita/matita/lib/lambda/terms/iterated_abstraction.ma index a4aa4f46f..2d05dc422 100644 --- a/matita/matita/lib/lambda/terms/iterated_abstraction.ma +++ b/matita/matita/lib/lambda/terms/iterated_abstraction.ma @@ -14,6 +14,8 @@ include "lambda/terms/term.ma". +include "lambda/notation/functions/annotatedabstraction_2.ma". + (* ITERATED ABSTRACTION *****************************************************) let rec abst d M on d ≝ match d with diff --git a/matita/matita/lib/lambda/terms/multiplicity.ma b/matita/matita/lib/lambda/terms/multiplicity.ma index 737ce634b..ebe35502d 100644 --- a/matita/matita/lib/lambda/terms/multiplicity.ma +++ b/matita/matita/lib/lambda/terms/multiplicity.ma @@ -14,6 +14,8 @@ include "lambda/terms/relocating_substitution.ma". +include "lambda/notation/functions/multiplicity_1.ma". + (* MULTIPLICITY *************************************************************) (* Note: this gives the number of variable references in M *) @@ -26,10 +28,6 @@ let rec mult M on M ≝ match M with interpretation "term multiplicity" 'Multiplicity M = (mult M). -notation "hvbox( ♯{ term 46 M } )" - non associative with precedence 90 - for @{ 'Multiplicity $M }. - lemma mult_positive: ∀M. 0 < ♯{M}. #M elim M -M // /2 width=1/ qed. diff --git a/matita/matita/lib/lambda/terms/parallel_computation.ma b/matita/matita/lib/lambda/terms/parallel_computation.ma index cd27b3c30..932eecf98 100644 --- a/matita/matita/lib/lambda/terms/parallel_computation.ma +++ b/matita/matita/lib/lambda/terms/parallel_computation.ma @@ -14,6 +14,8 @@ include "lambda/terms/parallel_reduction.ma". +include "lambda/notation/relations/parredstar_2.ma". + (* PARALLEL COMPUTATION (MULTISTEP) *****************************************) definition preds: relation term ≝ star … pred. diff --git a/matita/matita/lib/lambda/terms/parallel_reduction.ma b/matita/matita/lib/lambda/terms/parallel_reduction.ma index b2d2c2ff9..17313b537 100644 --- a/matita/matita/lib/lambda/terms/parallel_reduction.ma +++ b/matita/matita/lib/lambda/terms/parallel_reduction.ma @@ -15,6 +15,10 @@ include "lambda/terms/size.ma". include "lambda/terms/sequential_reduction.ma". +include "lambda/notation/relations/parred_2.ma". + +include "lambda/xoa/ex_4_3.ma". + (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) (* Note: the application "(A B)" is represented by "@B.A" diff --git a/matita/matita/lib/lambda/terms/relocating_substitution.ma b/matita/matita/lib/lambda/terms/relocating_substitution.ma index 826c458d7..cf0bed4e8 100644 --- a/matita/matita/lib/lambda/terms/relocating_substitution.ma +++ b/matita/matita/lib/lambda/terms/relocating_substitution.ma @@ -14,6 +14,8 @@ include "lambda/terms/relocation.ma". +include "lambda/notation/functions/dsubst_3.ma". + (* RELOCATING SUBSTITUTION **************************************************) (* Policy: depth (level) metavariables: d, e (as for lift) *) diff --git a/matita/matita/lib/lambda/terms/relocation.ma b/matita/matita/lib/lambda/terms/relocation.ma index 3d42e8a5c..dffa5b4d5 100644 --- a/matita/matita/lib/lambda/terms/relocation.ma +++ b/matita/matita/lib/lambda/terms/relocation.ma @@ -14,6 +14,8 @@ include "lambda/terms/term.ma". +include "lambda/notation/functions/lift_3.ma". + (* RELOCATION ***************************************************************) (* Policy: level metavariables : d, e diff --git a/matita/matita/lib/lambda/terms/sequential_computation.ma b/matita/matita/lib/lambda/terms/sequential_computation.ma index 717a7602a..8b32acd8a 100644 --- a/matita/matita/lib/lambda/terms/sequential_computation.ma +++ b/matita/matita/lib/lambda/terms/sequential_computation.ma @@ -14,6 +14,8 @@ include "lambda/terms/parallel_computation.ma". +include "lambda/notation/relations/seqredstar_2.ma". + (* SEQUENTIAL COMPUTATION (MULTISTEP) ***************************************) definition sreds: relation term ≝ star … sred. diff --git a/matita/matita/lib/lambda/terms/sequential_reduction.ma b/matita/matita/lib/lambda/terms/sequential_reduction.ma index f1a6bfaf8..ab5fd39dc 100644 --- a/matita/matita/lib/lambda/terms/sequential_reduction.ma +++ b/matita/matita/lib/lambda/terms/sequential_reduction.ma @@ -14,6 +14,8 @@ include "lambda/terms/multiplicity.ma". +include "lambda/notation/relations/seqred_2.ma". + (* SEQUENTIAL REDUCTION (SINGLE STEP) ***************************************) (* Note: the application "(A B)" is represented by "@B.A" following: diff --git a/matita/matita/lib/lambda/terms/term.ma b/matita/matita/lib/lambda/terms/term.ma index 9db0fffa8..5eefe2a57 100644 --- a/matita/matita/lib/lambda/terms/term.ma +++ b/matita/matita/lib/lambda/terms/term.ma @@ -16,6 +16,10 @@ include "lambda/background/preamble.ma". +include "lambda/notation/functions/variablereferencebyindex_1.ma". +include "lambda/notation/functions/abstraction_1.ma". +include "lambda/notation/functions/application_2.ma". + (* TERM STRUCTURE ***********************************************************) (* Policy: term metavariables : A, B, C, D, M, N diff --git a/matita/matita/lib/lambda/xoa.conf.xml b/matita/matita/lib/lambda/xoa.conf.xml index 2d188536d..817c86e7b 100644 --- a/matita/matita/lib/lambda/xoa.conf.xml +++ b/matita/matita/lib/lambda/xoa.conf.xml @@ -1,12 +1,9 @@ -
- $(MATITA_RT_BASE_DIR) -
- lib/ - lambda/background/xoa - lambda/background/xoa_notation + .. + lambda/xoa + lambda/notation/xoa basics/pts.ma 1 2 2 2 diff --git a/matita/matita/lib/lambda/xoa/ex_1_2.ma b/matita/matita/lib/lambda/xoa/ex_1_2.ma new file mode 100644 index 000000000..2ef4d92fd --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_1_2.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_1_2.ma". + +(* multiple existental quantifier (1, 2) *) + +inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ + | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? +. + +interpretation "multiple existental quantifier (1, 2)" 'Ex2 P0 = (ex1_2 ? ? P0). + diff --git a/matita/matita/lib/lambda/xoa/ex_2_2.ma b/matita/matita/lib/lambda/xoa/ex_2_2.ma new file mode 100644 index 000000000..f9eb911c3 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_2_2.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_2_2.ma". + +(* multiple existental quantifier (2, 2) *) + +inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ + | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 2)" 'Ex2 P0 P1 = (ex2_2 ? ? P0 P1). + diff --git a/matita/matita/lib/lambda/xoa/ex_2_3.ma b/matita/matita/lib/lambda/xoa/ex_2_3.ma new file mode 100644 index 000000000..fc16c6fcd --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_2_3.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_2_3.ma". + +(* multiple existental quantifier (2, 3) *) + +inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ + | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 3)" 'Ex3 P0 P1 = (ex2_3 ? ? ? P0 P1). + diff --git a/matita/matita/lib/lambda/xoa/ex_3_1.ma b/matita/matita/lib/lambda/xoa/ex_3_1.ma new file mode 100644 index 000000000..0655bc897 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_3_1.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_3_1.ma". + +(* multiple existental quantifier (3, 1) *) + +inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ + | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). + diff --git a/matita/matita/lib/lambda/xoa/ex_3_2.ma b/matita/matita/lib/lambda/xoa/ex_3_2.ma new file mode 100644 index 000000000..244b9c8eb --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_3_2.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_3_2.ma". + +(* multiple existental quantifier (3, 2) *) + +inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ + | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 2)" 'Ex2 P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). + diff --git a/matita/matita/lib/lambda/xoa/ex_3_3.ma b/matita/matita/lib/lambda/xoa/ex_3_3.ma new file mode 100644 index 000000000..b12de65da --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_3_3.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_3_3.ma". + +(* multiple existental quantifier (3, 3) *) + +inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ + | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 3)" 'Ex3 P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). + diff --git a/matita/matita/lib/lambda/xoa/ex_3_4.ma b/matita/matita/lib/lambda/xoa/ex_3_4.ma new file mode 100644 index 000000000..4d915a430 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_3_4.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_3_4.ma". + +(* multiple existental quantifier (3, 4) *) + +inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ + | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 4)" 'Ex4 P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). + diff --git a/matita/matita/lib/lambda/xoa/ex_4_1.ma b/matita/matita/lib/lambda/xoa/ex_4_1.ma new file mode 100644 index 000000000..b06fa54c5 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_4_1.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_4_1.ma". + +(* multiple existental quantifier (4, 1) *) + +inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ + | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). + diff --git a/matita/matita/lib/lambda/xoa/ex_4_2.ma b/matita/matita/lib/lambda/xoa/ex_4_2.ma new file mode 100644 index 000000000..0bc7ec5f4 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_4_2.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_4_2.ma". + +(* multiple existental quantifier (4, 2) *) + +inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ + | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 2)" 'Ex2 P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). + diff --git a/matita/matita/lib/lambda/xoa/ex_4_3.ma b/matita/matita/lib/lambda/xoa/ex_4_3.ma new file mode 100644 index 000000000..a4229001d --- /dev/null +++ b/matita/matita/lib/lambda/xoa/ex_4_3.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/ex_4_3.ma". + +(* multiple existental quantifier (4, 3) *) + +inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ + | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 3)" 'Ex3 P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). + diff --git a/matita/matita/lib/lambda/xoa/or_3.ma b/matita/matita/lib/lambda/xoa/or_3.ma new file mode 100644 index 000000000..f949c27c5 --- /dev/null +++ b/matita/matita/lib/lambda/xoa/or_3.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "lambda/notation/xoa/or_3.ma". + +(* multiple disjunction connective (3) *) + +inductive or3 (P0,P1,P2:Prop) : Prop ≝ + | or3_intro0: P0 → or3 ? ? ? + | or3_intro1: P1 → or3 ? ? ? + | or3_intro2: P2 → or3 ? ? ? +. + +interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). + -- 2.39.2