|
interval_expr_trig : THEORY
BEGIN
IMPORTING interval_expr,
interval_trig
expr : VAR RealExpr
n : VAR nat
pi_safe : [Unit->real] = LAMBDA(u:Unit) : pi
Pi_Inclusion : JUDGEMENT
Pi(n) HAS_TYPE (Includes?(pi_safe(unit)))
PI_n(n): MACRO RealExpr = CONST(pi_safe,Pi(n))
Sin_Inclusion : JUDGEMENT
Sin(n) HAS_TYPE (Inclusion?(PreTrue,sin))
Sin_Fundamental : JUDGEMENT
Sin(n) HAS_TYPE (Fundamental?(PreTrue))
SIN_n(n)(expr): MACRO RealExpr = FUN(PreTrue,sin,Sin(n),expr)
Cos_Inclusion : JUDGEMENT
Cos(n) HAS_TYPE (Inclusion?(PreTrue,cos))
Cos_Fundamental : JUDGEMENT
Cos(n) HAS_TYPE (Fundamental?(PreTrue))
COS_n(n)(expr): MACRO RealExpr = FUN(PreTrue,cos,Cos(n),expr)
tan_safe(x:real): real = IF Tan?(x) THEN tan(x) ELSE 0 ENDIF
Tan_Inclusion : JUDGEMENT
Tan(n) HAS_TYPE (Inclusion?(TAN?(n),tan_safe))
Tan_Fundamental : JUDGEMENT
Tan(n) HAS_TYPE (Fundamental?(TAN?(n)))
TAN_Precondition : JUDGEMENT
TAN?(n) HAS_TYPE (Precondition?)
TAN_n(n)(expr): MACRO RealExpr = FUN(TAN?(n),tan_safe,Tan(n),expr)
Atan_Inclusion : JUDGEMENT
Atan(n) HAS_TYPE (Inclusion?(PreTrue,atan))
Atan_Fundamental : JUDGEMENT
Atan(n) HAS_TYPE (Fundamental?(PreTrue))
ATAN_n(n)(expr): MACRO RealExpr = FUN(PreTrue,atan,Atan(n),expr)
END interval_expr_trig
¤ Dauer der Verarbeitung: 0.10 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.
|
