some renaming to free the baseuri cic:/matita/lambda

[helm.git] / matita / matita / lib / pts_dummy_new / lambda_notation.ma

diff --git a/matita/matita/lib/pts_dummy_new/lambda_notation.ma b/matita/matita/lib/pts_dummy_new/lambda_notation.ma
new file mode 100644 (file)
index 0000000..57c02e0
--- /dev/null
+++ b/matita/matita/lib/pts_dummy_new/lambda_notation.ma
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE LAMBDA CALCULUS *)
+(* equivalence, invariance *)
+
+notation "hvbox(a break ≅ b)" 
+  non associative with precedence 45
+  for @{'Eq $a $b}.
+
+notation "hvbox(a break (≅ ^ term 90 c) b)"
+  non associative with precedence 45
+  for @{'Eq1 $c $a $b}.
+
+notation "hbox(! term 55 a)"
+  non associative with precedence 55
+  for @{'Invariant $a}.
+
+notation "hbox((! ^ term 90 b) term 55 a)"
+  non associative with precedence 55
+  for @{'Invariant1 $a $b}.
+
+(* lifting, substitution *)
+
+notation "hvbox(↑ [ p break , k ] break t)"
+   non associative with precedence 55
+   for @{'Lift1 $p $k $t}.
+
+notation "hvbox(M break [ / l ])"
+   non associative with precedence 90
+   for @{'Subst $M $l}.
+
+notation "hvbox(M break [ k ≝ N ])" 
+   non associative with precedence 90
+   for @{'Subst1 $M $k $N}.
+
+(* type judgements *)
+
+notation "hvbox(G break  ⊢ A break : B)"
+   non associative with precedence 45
+   for @{'TJ $G $A $B}.
+
+notation "hvbox(G break  ⊢ A break ÷ B)"
+   non associative with precedence 45
+   for @{'TJ0 $G $A $B}.
+
+(* interpretations *)
+
+notation "hvbox(║T║)"
+   non associative with precedence 55
+   for @{'IInt $T}.
+
+notation "hvbox(║T║ break _ [E])"
+   non associative with precedence 55
+   for @{'IInt1 $T $E}.
+
+notation "hvbox(║T║ break _ [E1 break , E2])"
+   non associative with precedence 55
+   for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(〚T〛)"
+   non associative with precedence 55
+   for @{'EInt $T}.
+
+notation "hvbox(〚T〛 break _ [E])"
+   non associative with precedence 55
+   for @{'EInt1 $T $E}.
+
+notation "hvbox(〚T〛 break _ [E1 break , E2])"
+   non associative with precedence 55
+   for @{'EInt2 $T $E1 $E2}.
+
+notation "hvbox(《T》)"
+   non associative with precedence 55
+   for @{'XInt $T}.
+
+notation "hvbox(《T》 break _ [E])"
+   non associative with precedence 55
+   for @{'XInt1 $T $E}.
+
+notation "hvbox(《T》 break _ [E1 break , E2])"
+   non associative with precedence 55
+   for @{'XInt2 $T $E1 $E2}.