initial properies of the "same top term constructor" predicate

[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 f10f7b4f677abfde8c9a659debeb0380088f931b..7d05a2f6702028fc976b16b6724c8c4ce9bbc128 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -104,16 +104,36 @@ notation "hvbox( # [ x , break y ] )"
  non associative with precedence 90
  for @{ 'Weight $x $y }.
 
-notation "hvbox( ð\9d\95\8a [ T ] )"
+notation "hvbox( ð\9d\90\92 [ T ] )"
    non associative with precedence 45
    for @{ 'Simple $T }.
 
+notation "hvbox( L ⊢ break term 90 T1 ≈ break T2 )"
+   non associative with precedence 45
+   for @{ 'Hom $L $T1 $T2 }.
+
+notation "hvbox( T1 ≃ break T2 )"
+   non associative with precedence 45
+   for @{ 'Iso $T1 $T2 }.
+
 notation "hvbox( T1 break [ d , break e ] ≼ break T2 )"
    non associative with precedence 45
    for @{ 'SubEq $T1 $d $e $T2 }.
 
 (* Substitution *************************************************************)
 
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )"
+   non associative with precedence 45
+   for @{ 'Reducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )"
+   non associative with precedence 45
+   for @{ 'NotReducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )"
+   non associative with precedence 45
+   for @{ 'Normal $L $d $e $T }.
+
 notation "hvbox( ⇧ [ d , break e ] break T1 ≡ break T2 )"
    non associative with precedence 45
    for @{ 'RLift $d $e $T1 $T2 }.
@@ -180,51 +200,51 @@ notation "hvbox( T1 ÷ ⊑ break T2 )"
 
 (* Reducibility *************************************************************)
 
-notation "hvbox( ℝ [ T ] )"
+notation "hvbox( 𝐑 [ T ] )"
    non associative with precedence 45
    for @{ 'Reducible $T }.
 
-notation "hvbox( L ⊢ ℝ [ T ] )"
+notation "hvbox( L ⊢ break 𝐑 [ T ] )"
    non associative with precedence 45
    for @{ 'Reducible $L $T }.
 
-notation "hvbox( ð\9d\95\80 [ T ] )"
+notation "hvbox( ð\9d\90\88 [ T ] )"
    non associative with precedence 45
    for @{ 'NotReducible $T }.
 
-notation "hvbox( L ⊢ 𝕀 [ T ] )"
+notation "hvbox( L ⊢ break 𝐈 [ T ] )"
    non associative with precedence 45
    for @{ 'NotReducible $L $T }.
 
-notation "hvbox( ℕ [ T ] )"
+notation "hvbox( 𝐍 [ T ] )"
    non associative with precedence 45
    for @{ 'Normal $T }.
 
-notation "hvbox( L ⊢ ℕ [ T ] )"
+notation "hvbox( L ⊢ break 𝐍 [ T ] )"
    non associative with precedence 45
    for @{ 'Normal $L $T }.
 
-notation "hvbox( ð\9d\95\8eâ\84\8dâ\84\9d [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\91 [ T ] )"
    non associative with precedence 45
    for @{ 'WHdReducible $T }.
 
-notation "hvbox( L ⊢ 𝕎ℍℝ [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )"
    non associative with precedence 45
    for @{ 'WHdReducible $L $T }.
 
-notation "hvbox( ð\9d\95\8eâ\84\8dð\9d\95\80 [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\88 [ T ] )"
    non associative with precedence 45
    for @{ 'NotWHdReducible $T }.
 
-notation "hvbox( L ⊢ 𝕎ℍ𝕀 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐈 [ T ] )"
    non associative with precedence 45
    for @{ 'NotWHdReducible $L $T }.
 
-notation "hvbox( ð\9d\95\8eâ\84\8dâ\84\95 [ T ] )"
+notation "hvbox( ð\9d\90\96ð\9d\90\87ð\9d\90\8d [ T ] )"
    non associative with precedence 45
    for @{ 'WHdNormal $T }.
 
-notation "hvbox( L ⊢ 𝕎ℍℕ [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )"
    non associative with precedence 45
    for @{ 'WHdNormal $L $T }.
 
@@ -262,6 +282,10 @@ notation "hvbox( L ⊢ ⬇ * T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
 
+notation "hvbox( L ⊢ ⬇ * * T )"
+   non associative with precedence 45
+   for @{ 'SNStar $L $T }.
+
 notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
    non associative with precedence 45
    for @{ 'InEInt $R $L $T $A }.