- new component for restricted computation (delta, zeta and tau only)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / notation.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 9c9c19209357e58b563888a367fed8016b080207..5e730aec23eb5a335e09e06dc256c88840fbbc12 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -252,6 +252,16 @@ notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'Unwind $L1 $T $L2 }.
 
+(* Restricted ***************************************************************)
+
+notation "hvbox( L ⊢ break term 46 T1 ➤ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRestStar $L $T1 $T2 }.
+
+notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRestStarSn $T1 $T2 }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )"