The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello,

On Mon, 2018-02-26 at 18:04 -0500, Cao Qinxiang wrote:
> Is power function like the following one defined in Coq standard
> library?
> 
> Fixpoint pow_func {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
>  match n with
>   | O   => a
>   | S n => f (pow_func f n a)
> end.

There is a iter_nat notation.

Require Import Arith.
Locate  iter_nat.
Notation Coq.Arith.Wf_nat.iter_nat
Print iter_nat
Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n)

Best,
--
Frédéric