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 (* GENERIC NOTATION *********************************************************)
17 notation "hvbox( # term 90 i )"
18 non associative with precedence 46
19 for @{ 'VariableReferenceByIndex $i }.
21 notation "hvbox( { term 46 b } # break term 90 i )"
22 non associative with precedence 46
23 for @{ 'VariableReferenceByIndex $b $i }.
25 notation "hvbox( 𝛌 . term 46 A )"
26 non associative with precedence 46
27 for @{ 'Abstraction $A }.
29 notation "hvbox( { term 46 b } 𝛌 . break term 46 T)"
30 non associative with precedence 46
31 for @{ 'Abstraction $b $T }.
33 notation "hvbox( @ term 46 C . break term 46 A )"
34 non associative with precedence 46
35 for @{ 'Application $C $A }.
37 notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
38 non associative with precedence 46
39 for @{ 'Application $b $V $T }.
41 notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )"
42 non associative with precedence 46
43 for @{ 'Lift $h $d $M }.
45 notation > "hvbox( ↑ [ term 46 h ] break term 46 M )"
46 non associative with precedence 46
47 for @{ 'Lift $h 0 $M }.
49 notation > "hvbox( ↑ term 46 M )"
50 non associative with precedence 46
51 for @{ 'Lift 1 0 $M }.
53 (* Note: the notation with "/" does not work *)
54 notation "hvbox( [ term 46 d ↙ break term 46 N ] break term 46 M )"
55 non associative with precedence 46
56 for @{ 'DSubst $N $d $M }.
58 notation > "hvbox( [ ↙ term 46 N ] break term 46 M )"
59 non associative with precedence 46
60 for @{ 'DSubst $N 0 $M }.