1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/background/preamble.ma".
17 (* PER LEVEL TERM STRUCTURE *************************************************)
19 (* Policy: term metavariables : A, B, C, D, M, N
20 relative level metavariables: i, j
21 absolute level metavariables: d, e
23 (* Bote: first argument: relative level of the term *)
24 inductive lterm: Type[0] ≝
25 | LVRef: nat → nat → lterm (* variable reference by level *)
26 | LAppl: nat → lterm → lterm → lterm (* function application *)
29 interpretation "stratified term construction (variable reference by level)"
30 'VariableReferenceByLevel i d = (LVRef i d).
32 interpretation "stratified term construction (application)"
33 'Application i C A = (LAppl i C A).
35 notation "hvbox( { term 46 b } § break term 90 d )"
36 non associative with precedence 46
37 for @{ 'VariableReferenceByLevel $b $d }.