arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / pnat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 53d5236f340fa4d455dcb2fa7eda3c904b00f390..e6db03ac46b8cccce12764f84693c9a8e461dc74 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -20,7 +20,7 @@ definition pplus: pnat → pnat → pnat ≝
            λp,q. psucc^q p.
 
 interpretation
-  "plus (positive integers"
+  "plus (positive integers)"
   'plus p q = (pplus p q).
 
 (* Basic rewrites ***********************************************************)