- notation fix for reducible and normal forms

[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..c25341f636039a0c68e90e518cd8a1cd5e4894c7 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -104,7 +104,7 @@ 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 }.
 
@@ -114,6 +114,18 @@ notation "hvbox( T1 break [ d , break e ] ≼ break 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 +192,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 }.