|
listn[T:TYPE] : THEORY
BEGIN
IMPORTING list[T]
listn?(n:nat)(l:list) : MACRO bool = length(l)=n
listn(n:nat) : TYPE = (listn?(n))
listn_ext : LEMMA
FORALL(n:nat,l1:listn(n),l2:listn(n)):
(FORALL (i:below(n)): nth(l1,i) = nth(l2,i)) IMPLIES l1 = l2
listn_0 : JUDGEMENT
null HAS_TYPE listn(0)
setnth(l:list,n:nat,f:[T->T]) : RECURSIVE
{sl : listn(length(l)) |
FORALL (i:below(length(l))) : IF i=n THEN nth(sl,i) = f(nth(l,i))
ELSE nth(sl,i) = nth(l,i)
ENDIF} =
CASES l OF
null : null,
cons(a,r) : IF n=0 THEN cons(f(a),r)
ELSE cons(a,setnth(r,n-1,f))
ENDIF
ENDCASES
MEASURE l BY <<
finseqn?(n:nat)(f:finseq[T]) : MACRO bool = f`length = n
Finseqn(n:nat) : TYPE = (finseqn?(n))
normalize_fseq(f:finseq[T]): {fsn: Finseqn(f`length)|fsn = f} =
LET fslist = finseq2list(f)
IN list2finseq(fslist)
normalize_fseq_def: LEMMA FORALL (f:finseq[T]): normalize_fseq(f) = f
END listn
¤ Dauer der Verarbeitung: 0.17 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.
|
