From e58a16408ecab0cdea0be912b9691ae03acdcc3b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 22 Nov 2012 16:09:47 +0000 Subject: [PATCH] a development about pure lambda calculus --- matita/matita/contribs/lambda/root | 1 + matita/matita/contribs/lambda/term.ma | 48 +++++++++++++++++++++++++++ 2 files changed, 49 insertions(+) create mode 100644 matita/matita/contribs/lambda/root create mode 100644 matita/matita/contribs/lambda/term.ma 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-. -- 2.39.2