theory Example imports "../LTL""../Rewriting""HOL-Library.Code_Target_Numeral" begin
―‹The included parser always returns a @{typ "String.literal ltlc"}. If a different labelling
is needed one can use @{const map_ltlc} to relabel the leafs. In our example we prepend a
string to each atom.›
definition rewrite :: "String.literal ltlc ==> String.literal ltlc" where "rewrite ≡ ltln_to_ltlc o rewrite_iter_slow o ltlc_to_ltln o (map_ltlc (λs. String.implode ''prop('' + s + String.implode '')''))"
―‹Export rewriting engine (and also constructors)›
export_code truec Iff_ltlc rewrite in SML file_prefix ‹rewrite_example›
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.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
