| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Circus/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 1020 B |
|
Quellcode-Bibliothek Var.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
section ‹UTP variables› theory Var imports Main begin text ‹UTP variables are characterized by two functions, $select$ and $update$. The variable type is then defined as a tuple ($select$ * $update$).› type_synonym ('a, 'r) var = "('r → 'a) * (('a → 'a) → 'r → 'r)" text ‹The $lookup$ function returns the corrsponding $select$ function of a varia definition lookup :: "('a, 'r) var → 'r → 'a" where "lookup f ≡ (fst f)" text ‹The $assign$ function uses the $update$ function of a variable to update it definition assign :: "('a, 'r) var → 'a → 'r → 'r" where "assign f v ≡ (snd f) (λ _ . v)" text ‹The $VAR$ function allows to retrieve a variable given its name.› syntax "_VAR" :: "id → ('a, 'r) var" (‹VAR _›) translations "VAR x" => "(x, _update_name x)" end
¤ 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 am 2026-11-04) ¤*Bot Zugriff |
|
||||||||||||||||||||||||
2026-11-01