]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/term.ma
a38508ada1ad1b2ba469ab16057417eb98ee1d90
[helm.git] / matita / matita / contribs / lambda / term.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* Initial invocation: - Patience on us to gain peace and perfection! - *)
16
17 include "preamble.ma".
18
19 (* TERM STRUCTURE ***********************************************************)
20
21 (* Policy: term metavariables: A, B, C, D, M, N
22            de Bruijn indexes : i, j
23 *)
24 inductive term: Type[0] ≝
25 | VRef: nat → term         (* variable reference by index *)
26 | Abst: term → term        (* function formation          *)
27 | Appl: term → term → term (* function application        *)
28 .
29
30 interpretation "term construction (variable reference by index)"
31    'VariableReferenceByIndex i = (VRef i).
32
33 interpretation "term construction (abstraction)"
34    'Abstraction A = (Abst A).
35
36 interpretation "term construction (application)"
37    'Application C A = (Appl C A).
38
39 notation "hvbox( # term 90 i )"
40  non associative with precedence 55
41  for @{ 'VariableReferenceByIndex $i }.
42
43 notation "hvbox( 𝛌  . term 55 A )"
44    non associative with precedence 55
45    for @{ 'Abstraction $A }.
46
47 notation > "hvbox( 𝛌 term 55 A )"
48    non associative with precedence 55
49    for @{ 'Abstraction $A }.
50
51 notation "hvbox( @ term 55 C . break term 55 A )"
52    non associative with precedence 55
53    for @{ 'Application $C $A }.