(* Title: HOL/Statespace/StateSpaceSyntax.thy Author: Norbert Schirmer, TU Muenchen \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close> theory StateSpaceSyntaximports StateSpaceLocalebegin text \<open>The state space syntax is kept in an extra theory so that you if you want to use it or not.\<close> 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" == "_statespace_update s x y" parse_translation \<open> \<^syntax_const>\<open>_statespace_lookup\<close>, StateSpace.lookup_tr), \<^syntax_const>\<open>_statespace_update\<close>, StateSpace.update_tr)] \<close> print_translation \<open> \<^const_syntax>\<open>lookup\<close>, StateSpace.lookup_tr'), \<^const_syntax>\<open>update\<close>, StateSpace.update_tr')] \<close> end quality 84%
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
