--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-.
(* *)
(**************************************************************************)
-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] โ
- | 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).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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).
--- /dev/null
+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 @, ,$*))
+
'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
projects / helm.git / commitdiff