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 (* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
17 (* equivalence, invariance *)
19 notation "hvbox(a break ≅ b)"
20 non associative with precedence 45
23 notation "hvbox(a break (≅ ^ term 90 c) b)"
24 non associative with precedence 45
27 notation "hbox(! term 50 a)"
28 non associative with precedence 50
31 notation "hbox((! ^ term 90 b) term 50 a)"
32 non associative with precedence 50
33 for @{'Invariant1 $a $b}.
35 (* lifting, substitution *)
37 notation "hvbox(↑ [ p break , k ] break t)"
38 non associative with precedence 50
39 for @{'Lift1 $p $k $t}.
41 notation "hvbox(M break [ / l ])"
42 non associative with precedence 90
45 notation "hvbox(M break [ k ≝ N ])"
46 non associative with precedence 90
47 for @{'Subst1 $M $k $N}.
51 notation "hvbox(G break ⊢ A break : B)"
52 non associative with precedence 45
55 notation "hvbox(G break ⊢ A break ÷ B)"
56 non associative with precedence 45
62 non associative with precedence 50
65 notation "hvbox(║T║ break _ [E])"
66 non associative with precedence 50
69 notation "hvbox(║T║ break _ [E1 break , E2])"
70 non associative with precedence 50
71 for @{'IInt2 $T $E1 $E2}.
74 non associative with precedence 50
77 notation "hvbox(〚T〛 break _ [E])"
78 non associative with precedence 50
81 notation "hvbox(〚T〛 break _ [E1 break , E2])"
82 non associative with precedence 50
83 for @{'EInt2 $T $E1 $E2}.
86 non associative with precedence 50
89 notation "hvbox(《T》 break _ [E])"
90 non associative with precedence 50
93 notation "hvbox(《T》 break _ [E1 break , E2])"
94 non associative with precedence 50
95 for @{'XInt2 $T $E1 $E2}.