lambda_delta: global environments handling: redefined and first results

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / notation.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index 36f9f765294632f4ee1df6ab3d9e24acad4f8b16..f528a9062236fe15d6a46490aaf4bb4847974575 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -68,6 +68,10 @@ notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )"
  non associative with precedence 89
  for @{ 'DBind $T $I $T1 }.
 *) (**) (* this breaks all parsing *)
+notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )"
+ non associative with precedence 47
+ for @{ 'DBind $T $I $T1 $T2 $T3 }.
+
 notation "hvbox( # [ x ] )"
  non associative with precedence 90
  for @{ 'Weight $x }.