]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/lambda/lambda_notation.ma
- nnAuto.ml: width overflows are warnings, not errors
[helm.git] / matita / matita / lib / lambda / lambda_notation.ma
index 4f2f4f1dc5334a5308fc7e96bcef2a896d165b61..8063634d0a3210410d4c98ed31b1dcfae41bb3dd 100644 (file)
@@ -97,6 +97,10 @@ notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
 
-notation "hvbox(𝕂{T} break _ [E])"
+notation "hvbox(𝕂{G})"
    non associative with precedence 50
-   for @{'IK1 $T $E}.
+   for @{'IK $G}.
+
+notation "hvbox(𝕂{T} break _ [G])"
+   non associative with precedence 50
+   for @{'IK $T $G}.