- degree: some improvements and the Deg_append lemma

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

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 596424938e459fb0e62d51f5e8fd0bc5d13b475b..e8ca08046d97164ea86bd987624231f01bb1940b 100644 (file)
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -92,3 +92,7 @@ notation "hvbox(《T》 break _ [E])"
 notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
+
+notation "hvbox(𝕂{T} break _ [E])"
+   non associative with precedence 50
+   for @{'IK1 $T $E}.