summaryrefslogtreecommitdiff
path: root/theories/Reals/Rpow_def.v
blob: 5bdbb76b98ef8cf613f7f6929b07dd58abcab571 (plain)
1
2
3
4
5
6
7
Require Import Rdefinitions.

Fixpoint pow (r:R) (n:nat) {struct n} : R :=
  match n with
    | O => R1
    | S n => Rmult r (pow r n)
  end.