X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=4f2f4f1dc5334a5308fc7e96bcef2a896d165b61;hb=a6602de6db0993a67c5b23aedb3c8fe1d484855f;hp=e8ca08046d97164ea86bd987624231f01bb1940b;hpb=ec401f51799a051fe8935b36d589fca5a4728d81;p=helm.git diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma index e8ca08046..4f2f4f1dc 100644 --- a/matita/matita/lib/lambda/lambda_notation.ma +++ b/matita/matita/lib/lambda/lambda_notation.ma @@ -69,6 +69,10 @@ notation "hvbox(║T║ break _ [E1 break , E2])" non associative with precedence 50 for @{'IInt2 $T $E1 $E2}. +notation "hvbox(║T║ * break _ [E])" + non associative with precedence 50 + for @{'IIntS1 $T $E}. + notation "hvbox(〚T〛)" non associative with precedence 50 for @{'EInt $T}.