| products/sources/formale Sprachen/Coq/library/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: usage.mli Sprache: PVSOriginal von: PVS© |
|
||||||
|
fsq[T: TYPE]: THEORY
%------------------------------------------------------------------------ % % This theory is scaffolding for the "fseqs" finite sequences theory % %------------------------------------------------------------------------ BEGIN x,y : VAR T fsq: TYPE = [# length: nat, seq: [nat -> T] #] cnvfsq(fs: fsq): MACRO [nat -> T] = fs`seq; CONVERSION cnvfsq; CONVERSION- finseq_appl; %% turn off prelude finseq conversion l(f: fsq): MACRO nat = f`length seqn(f: fsq): MACRO [nat -> T]= f`seq %% not empty fseqs ne_fsq: TYPE = {s: fsq | length(s) > 0} in?(x: T, s: fsq): bool = (EXISTS (ii: below(length(s))): x = seq(s)(ii)) fsq1(t:T): fsq = (# length := 1, seq := (LAMBDA (n: nat): t) #) const_fsq(n: nat,c:T): fsq = (# length := n, seq := (LAMBDA (n: nat): c) #) END fsq ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
