arithmetics for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index a749c5339d0a653b3027025b3f957e5e9966b556..9e806cfe2cf5d91612027727dfc57cc79d70405c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -15,7 +15,7 @@
 include "ground/notation/functions/exp_3.ma".
 include "ground/arith/pnat.ma".
 
-(* POSITIVE INTEGERS ********************************************************)
+(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
 
 rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
 match p with