|
%------------------------------------------------------------------------------
% 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
sign(f): [T->real] = lambda x: sign(f(x));
^(g,a): [T->nnreal] = lambda x: g(x)^a;
expt(f,n):[T->real] = lambda x: expt(f(x),n)
END real_fun_power
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
