fseqs_ops_real: THEORY %------------------------------------------------------------------------ % % Defines some convenient operations over finite sequences of reals % % EXPERIMENTAL % %------------------------------------------------------------------------ BEGIN
IMPORTING fseqs_ops[real]
fs,gs: VAR fseq
nefs: VAR ne_fseq
i,n: VAR nat
x: VAR real
nn_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) >= 0}
pos_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) > 0}
neg_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) < 0}
nz_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) /= 0}
% ------------ pointwise addition, subtraction, and multiplication
mmin(m,n:nat): MACRO nat = IF m > n THEN n ELSE m ENDIF ;
+(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
(# length := len,
seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) ELSE default ENDIF)
#) ;
-(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
(# length := len,
seq := (LAMBDA n: IF n < len THEN fs(n) - gs(n) ELSE default ENDIF)
#) ;
*(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN
(# length := len,
seq := (LAMBDA n: IF n < len THEN fs(n) * gs(n) ELSE default ENDIF)
#) ;
nzgs: VAR nz_fseq ;
/(fs,nzgs): fseq = LET len = mmin(l(fs),l(nzgs)) IN
(# length := len,
seq := (LAMBDA n: IF n < len THEN fs(n) / nzgs(n) ELSE default ENDIF)
#) ;
END fseqs_ops_real
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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.
