| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Hoare_Time/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 515 B |
|
Quelle BExp.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
theory BExp imports AExp begin subsection "Boolean Expressions" datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp fun bval :: "bexp → state → bool" where "bval (Bc v) s = v" | "bval (Not b) s = (¬ bval b s)" | "bval (And b1 b2) s = (bval b1 s ∧ bval b2 s)" | "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) <''x'' := 3, ''y'' := 1>" end
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01