| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/JinjaThreads/J/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 787 B |
|
Quelle State.thySprache: Isabelle |
|||||||||||||||
|
(* Title: JinjaThreads/J/State.thy Author: Tobias Nipkow, Andreas Lochbihler *) chapter ‹JinjaThreads source language› section ‹Program State› theory State imports "../Common/Heap" begin type_synonym 'addr locals = "vname ⇀ 'addr val" ― ‹local vars, incl. params and ``this''› type_synonym ('addr, 'heap) Jstate = "'heap × 'addr locals" ― ‹the heap and the local vars› definition hp :: "'heap × 'x ==> 'heap" where "hp ≡ fst" definition lcl :: "'heap × 'x ==> 'x" where "lcl ≡ snd" lemma hp_conv [simp]: "hp (h, l) = h" by(simp add: hp_def) lemma lcl_conv [simp]: "lcl (h, l) = l" by(simp add: lcl_def) end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09