|
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.0 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.
|
