Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Stdlib.Reals.Rpow_def
Require
Import
Rdefinitions
.
Fixpoint
pow
(
r
:
R
) (
n
:
nat
) :
R
:=
match
n
with
|
O
=> 1
|
S
n
=>
Rmult
r
(
pow
r
n
)
end
.
Navigation
Standard Library
Table of contents
Index