| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Statespace/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle StateSpaceSyntax.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/Statespace/StateSpaceSyntax.thy Author: Norbert Schirmer, TU Muenchen *) section ‹Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}› theory StateSpaceSyntax imports StateSpaceLocale begin text ‹The state space syntax is kept in an extra theory so that you choose if you want to use it or not.› syntax "_statespace_lookup" :: "('a → 'b) → 'a → 'c" (‹_⋅_› [60, 60] 60) "_statespace_update" :: "('a → 'b) → 'a → 'c → ('a → 'b)" "_statespace_updates" :: "('a → 'b) → updbinds → ('a → 'b)" (‹_🚫› [900, 0] 900) translations "_statespace_updates f (_updbinds b bs)" == "_statespace_updates (_statespace_updates f b) bs" "s<x:=y>" == "_statespace_update s x y" parse_translation ‹ [(syntax_const‹_statespace_lookup›, StateSpace.lookup_tr), (syntax_const‹_statespace_update›, StateSpace.update_tr)] › print_translation ‹ [(const_syntax‹lookup›, StateSpace.lookup_tr'), (const_syntax‹update›, StateSpace.update_tr')] › end
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09