X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fnat%2Fplus.ma;h=8bbc71b9cbbbc3b5d50ece774467c69ebf890048;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hp=75268ffcb4336b3ca709e5134dd51ae00c350a88;hpb=c6d3537eee27d05490a9555cc7326bc954b356c5;p=helm.git

diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma
index 75268ffcb..8bbc71b9c 100644
--- a/helm/software/matita/nlibrary/nat/plus.ma
+++ b/helm/software/matita/nlibrary/nat/plus.ma
@@ -21,6 +21,8 @@ nlet rec plus (n:nat) (m:nat) on n : nat ≝
   [ O ⇒ m
   | S n' ⇒ S (plus n' m) ].
 
+interpretation "natural plus" 'plus x y = (plus x y).
+
 ndefinition plus_magma_type: magma_type.
  napply mk_magma_type
   [ napply NAT
@@ -52,4 +54,4 @@ ndefinition plus_unital_magma_type: unital_magma_type.
   | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
 nqed.
 
-ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.
\ No newline at end of file
+ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.