update in alpha_1

+ type of terms redefined
+ Makefile added to lambdadelta/bin
+ a correction static_2/syntax/term.ma

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma
new file mode 100644 (file)
index 0000000..163477e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabst_1.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 FOR THE FORMAL SYSTEM λα ****************************************)
+
+notation "hvbox( ⓛ term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnAbst $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma
deleted file mode 100644 (file)
index 72707b0..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( -𝛌. break term 55 T )"
- non associative with precedence 55
- for @{ 'SnAbstNeg $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma
deleted file mode 100644 (file)
index 28f6c95..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( § term 90 l. break term 55 T )"
- non associative with precedence 55
- for @{ 'SnGRef $l $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma
deleted file mode 100644 (file)
index 130526c..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( ① [ term 46 I ]. break term 55 T )"
- non associative with precedence 55
- for @{ 'SnItem1 $I $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma
deleted file mode 100644 (file)
index 89516d4..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( # term 90 i. break term 55 T )"
- non associative with precedence 55
- for @{ 'SnLRef $i $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma
deleted file mode 100644 (file)
index 219df4d..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( 𝛑[ term 46 p ] break term 55 T1. break term 55 T2 )"
- non associative with precedence 55
- for @{ 'SnProj $p $T1 $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma
deleted file mode 100644 (file)
index 5ed5322..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( -𝛑 term 55 T1. break term 55 T2 )"
- non associative with precedence 55
- for @{ 'SnProjNeg $T1 $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma
deleted file mode 100644 (file)
index a1b9213..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( +𝛑 term 55 T1. break term 55 T2 )"
- non associative with precedence 55
- for @{ 'SnProjPos $T1 $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma
deleted file mode 100644 (file)
index c16c15c..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
-
-notation "hvbox( ⋆ term 90 s. break term 55 T )"
- non associative with precedence 55
- for @{ 'SnStar $s $T }.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma
deleted file mode 100644 (file)
index 7f7441d..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/item.ma
+++ /dev/null
@@ -1,38 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* THE FORMAL SYSTEM α: MATITA SOURCE FILES
- * Initial invocation : - Patience on me to gain peace and perfection! -
- * Developed since    : 2014 July 25
- *)
-
-include "ground/lib/bool.ma".
-include "ground/lib/arith.ma".
-
-(* ITEMS ********************************************************************)
-
-(* unary items *)
-inductive item1: Type[0] ≝
-   | Char: nat → item1 (* character: starting at 0 *)
-   | LRef: nat → item1 (* reference by index: starting at 0 *)
-   | GRef: nat → item1 (* reference by position: starting at 0 *)
-   | Decl:       item1 (* global abstraction *)
-.
-
-(* binary items *)
-inductive item2: Type[0] ≝
-   | Abst:        item2 (* local abstraction *)
-   | Abbr: bool → item2 (* local (Ⓣ) or global (Ⓕ) abbreviation *)
-   | Proj: bool → item2 (* local (Ⓣ) or global (Ⓕ) projection *)
-.

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
index 4334a09188fdc805314f2bcec4f1e1e944c64250..697150232a623f8601c761b1e54a81580ee284de 100644 (file)
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
+++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma
@@ -12,69 +12,46 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "static_2/notation/functions/snitem2_3.ma".
-include "static_2/notation/functions/star_0.ma".
-include "static_2/notation/functions/snabstpos_2.ma".
-include "static_2/notation/functions/snabbr_3.ma".
-include "static_2/notation/functions/snabbrpos_2.ma".
-include "static_2/notation/functions/snabbrneg_2.ma".
-include "alpha_1/notation/functions/snitem1_2.ma".
-include "alpha_1/notation/functions/snstar_2.ma".
-include "alpha_1/notation/functions/snlref_2.ma".
-include "alpha_1/notation/functions/sngref_2.ma".
-include "alpha_1/notation/functions/snabstneg_1.ma".
-include "alpha_1/notation/functions/snproj_3.ma".
-include "alpha_1/notation/functions/snprojpos_2.ma".
-include "alpha_1/notation/functions/snprojneg_2.ma".
-include "alpha_1/syntax/item.ma".
+(* THE FORMAL SYSTEM λα: MATITA SOURCE FILES
+ * Initial invocation: - Patience on me to gain peace and perfection! -
+ * Conceived since: 2014 July 25
+ * Developed since: 2021 June 17
+ *)
+
+include "ground/arith/nat.ma".
+include "static_2/notation/functions/star_1.ma".
+include "static_2/notation/functions/gref_1.ma".
+include "static_2/notation/functions/snappl_2.ma".
+include "static_2/notation/functions/snabbr_2.ma".
+include "alpha_1/notation/functions/snabst_1.ma".

 
 (* TERMS ********************************************************************)
 
 (* terms *)
 inductive term: Type[0] ≝
 
 (* TERMS ********************************************************************)
 
 (* terms *)
 inductive term: Type[0] ≝

-  | TAtom:         term                (* atomic item construction *)
-  | TUnit: item1 → term → term         (* unary item construction *)
-  | TPair: item2 → term → term → term  (* binary item construction *)
+  | TChar: nat → term          (* character: starts at 0 *)
+  | TGRef: nat → term          (* reference by level: starts at 0 *)
+  | TAbst: term → term         (* abstraction: scope *)
+  | TAbbr: term → term → term  (* abbreviation: definition, scope *)
+  | TCons: term → term → term  (* group: body, tail *) 

 .
 
 .
 

-interpretation "top (term)"
-   'Star = TAtom.
+interpretation
+  "character (terms)"
+  'Star c = (TChar c).

 
 

-interpretation "term construction (unary)"
-   'SnItem1 I T = (TUnit I T).
+interpretation
+  "reference (terms)"
+  'GRef l = (TGRef l).

 
 

-interpretation "term construction (binary)"
-   'SnItem2 I T1 T2 = (TPair I T1 T2).
+interpretation
+  "group (terms)"
+  'SnAppl T1 T2 = (TCons T1 T2).

 
 

-interpretation "character (term)"
-   'SnStar s T = (TUnit (Char s) T).
+interpretation
+  "abbreviation (terms)"
+  'SnAbbr T1 T2 = (TAbbr T1 T2).

 
 

-interpretation "local reference (term)"
-   'SnLRef i T = (TUnit (LRef i) T).
-
-interpretation "global reference (term)"
-   'SnGRef l T = (TUnit (GRef l) T).
-
-interpretation "negative abbreviation (term)"
-   'SnAbbrNeg T = (TUnit Decl T).
-
-interpretation "positive abstraction (term)"
-   'SnAbstPos T1 T2 = (TPair Abst T1 T2).
-
-interpretation "abbreviation (term)"
-   'SnAbbr p T1 T2 = (TPair (Abbr p) T1 T2).
-
-interpretation "positive abbreviation (term)"
-   'SnAbbrPos T1 T2 = (TPair (Abbr true) T1 T2).
-
-interpretation "negative abbreviation (term)"
-   'SnAbbrNeg T1 T2 = (TPair (Abbr false) T1 T2).
-
-interpretation "projection (term)"
-   'SnProj p T1 T2 = (TPair (Proj p) T1 T2).
-
-interpretation "positive projection (term)"
-   'SnProjPos T1 T2 = (TPair (Proj true) T1 T2).
-
-interpretation "negative projection (term)"
-   'SnProjNeg T1 T2 = (TPair (Proj false) T1 T2).
+interpretation
+  "abstraction (terms)"
+  'SnAbst T = (TAbst T).

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
deleted file mode 100644 (file)
index 63ddda1..0000000
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
+++ /dev/null
@@ -1,25 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "alpha_1/syntax/term.ma".
-
-(* TERMS ********************************************************************)
-
-let rec tappend T U on T ≝ match T with
-[ TAtom       ⇒ U
-| TUnit I T   ⇒ ①[I].(tappend T U)
-| TPair I V T ⇒ ②[I]V.(tappend T U)
-].
-
-interpretation "append (term)" 'plus T U = (tappend T U).

diff --git a/matita/matita/contribs/lambdadelta/bin/Makefile b/matita/matita/contribs/lambdadelta/bin/Makefile
new file mode 100644 (file)
index 0000000..74274dd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/Makefile
@@ -0,0 +1,10 @@
+H=@
+
+BINARIES = inline xhtbl index roles recomm
+
+all: $(BINARIES:%=rec@all@%)
+clean: $(BINARIES:%=rec@clean@%) 
+
+rec@%:
+       $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
+

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
index 0a6f97872a2e199d22d582cc0b087b8edadae198..cec29d172aff8ac95e845e825ce3a9f7e09b740d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
@@ -49,7 +49,7 @@ interpretation
   'SnItem2 I T1 T2 = (TPair I T1 T2).
 
 interpretation
   'SnItem2 I T1 T2 = (TPair I T1 T2).
 
 interpretation

-   "term binding construction (binary)"
+  "term binding construction (binary)"

   'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2).
 
 interpretation
   'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2).
 
 interpretation