- lambda_delta: static type assignment is defined

[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 7be9b8ecbf4a0f71535470dc9cefc585fc762fdf..dc4bda3964f7604728ef139cd78a4349153cdcce 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -192,7 +192,7 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $L $T1 $d $e $T2 }.
 
-(* Static Typing ************************************************************)
+(* Static typing ************************************************************)
 
 notation "hvbox( L ⊢ break term 90 T ÷ break A )"
    non associative with precedence 45
@@ -202,6 +202,16 @@ notation "hvbox( T1 ÷ ⊑ break T2 )"
    non associative with precedence 45
    for @{ 'CrSubEqA $T1 $T2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 • break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticType $h $L $T1 $T2 }.
+
+(* Unwind *******************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 •* break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticTypeStar $h $L $T1 $T2 }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( 𝐑 [ T ] )"
@@ -322,7 +332,7 @@ notation "hvbox( T1 ⊢ ⬌* break T2 )"
    non associative with precedence 45
    for @{ 'CPConvStar $T1 $T2 }.
 
-(* Native typing ************************************************************)
+(* Dynamic typing ***********************************************************)
 
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
    non associative with precedence 45