From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 22 Nov 2012 16:09:47 +0000 (+0000)
Subject: a development about pure lambda calculus
X-Git-Tag: make_still_working~1450
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e58a16408ecab0cdea0be912b9691ae03acdcc3b;p=helm.git

a development about pure lambda calculus
---

diff --git a/matita/matita/contribs/lambda/root b/matita/matita/contribs/lambda/root
new file mode 100644
index 000000000..183f1bc68
--- /dev/null
+++ b/matita/matita/contribs/lambda/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/lambda/
diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma
new file mode 100644
index 000000000..80a1de667
--- /dev/null
+++ b/matita/matita/contribs/lambda/term.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "arithmetics/nat.ma".
+
+(* Policy: term metavariables: A, B, C, D
+           de Bruijn indexes : i, j, h, k
+*)
+inductive term: Type[0] ≝
+| VRef: nat → term         (* variable reference by index, starts at zero *)
+| Abst: term → term        (* function formation *)
+| Appl: term → term → term (* function application, argument comes first *)
+.
+
+notation "hvbox( # term 90 i )"
+ non associative with precedence 55
+ for @{ 'VariableReferenceByIndex $i }.
+
+interpretation "term construction (variable reference by index)"
+   'VariableReferenceByIndex i = (VRef i).
+
+notation "hvbox( 𝛌 term 55 A )"
+   non associative with precedence 55
+   for @{ 'Abstraction $A }.
+
+interpretation "term construction (abstraction)"
+   'Abstraction A = (Abst A).
+
+notation "hvbox( @ term 55 C . break term 55 A )"
+   non associative with precedence 55
+   for @{ 'Application $C $A }.
+
+interpretation "term construction (application)"
+   'Application C A = (Appl C A).
+
+lemma prova_notazione: ∀A,i. @A.𝛌#i = @A.𝛌#i.
+// qed-.