seqs[T: TYPE]: THEORY
BEGIN
l(f: finite_sequence[T]): MACRO nat = f`length
ne_seqs: TYPE = {s: finite_sequence[T] | length(s) > 0}
in?(x: T, s: finite_sequence[T]): bool =
(EXISTS (ii: below(length(s))): x = seq(s)(ii))
const_seq(n: nat,c:T): finite_sequence[T] = (# length := n,
seq := (LAMBDA (i: below(n)): c) #)
seq1(t:T): ne_seqs = (# length := 1,
seq := (LAMBDA (n: below(1)): t)
#)
seq2(a,b:T): ne_seqs = (# length := 2,
seq := (LAMBDA (n: below(2)): IF n < 1 THEN a
ELSE b ENDIF)
#)
t: VAR T
seq1_def: LEMMA seq1(t)`seq(0) = t
AUTO_REWRITE+ seq1_def
fs: VAR finite_sequence[T]
rev(fs): finite_sequence[T] = (# length := l(fs),
seq := (LAMBDA (i: below(l(fs))): seq(fs)(l(fs)-1-i))
#)
add1(fs,t): finite_sequence[T] = (# length := l(fs) + 1,
seq := (LAMBDA (ii: below(l(fs)+1)):
IF ii < l(fs) THEN seq(fs)(ii)
ELSE t
ENDIF)
#)
END seqs
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
