%------------------------------------------------------------------------------ % Exponentials of functions % % Author: David Lester, Manchester University & NIA % % Version 1.0 15/09/08 Initial version (DRL) % % Note carefully that f^a is actually |f|^a. If you want $f^(1/3)$ to % be $\root[3]{f(x)}$, write it as $sign(f) * f^(1/3)$. % %------------------------------------------------------------------------------
real_fun_power[T:TYPE]: THEORY
BEGIN
IMPORTING reals@sign,
real_expt
f: VAR [T->real]
g: VAR [T->nnreal]
a: VAR posreal
x: VAR T
n: VAR nat
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
