| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 1009 B |
|
Impressum arrays.pvs Sprache: PVS |
|||||||||
|
arrays[N:nat] : THEORY
BEGIN Index : TYPE = below(N) Reals : TYPE = ARRAY[Index->real] Booleans : TYPE = ARRAY[Index->boolean] Bools : TYPE = Booleans Strings : TYPE = ARRAY[Index->string] Nats : TYPE = ARRAY[Index->nat] Ints : TYPE = ARRAY[Index->int] Rats : TYPE = ARRAY[Index->rat] ArrayOf[T:TYPE] : TYPE = ARRAY[Index->T] i : VAR Index length(r:Reals) : nat = N init_with(r:real) : Reals = LAMBDA(i):r length(q:Rats) : nat = N init_with(q:rat) : Rats = LAMBDA(i):q length(z:Ints) : nat = N init_with(z:int) : Ints = LAMBDA(i):z length(n:Nats) : nat = N init_with(n:nat) : Nats = LAMBDA(i):n init : MACRO Nats = init_with(0) length(b:Bools) : nat = N init_with(b:bool) : Bools = LAMBDA(i):b init : MACRO Bools = init_with(false) length(s:Strings) : nat = N init_with(s:string) : Strings = LAMBDA(i):s init : MACRO Strings = init_with("") length[T:TYPE](a:ArrayOf[T]) : nat = N init_with[T:TYPE](t:T) : ArrayOf[T] = LAMBDA(i):t END arrays ¤ 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.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28