Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Further explain evaluator option syntax for value_ text antiquotation
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2023-01-09 15:34:59 +01:00
parent 17ec11b297
commit 72d8000f7b
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -701,6 +701,11 @@ term antiquotations:
\<^item> \<^theory_text>\<open>@{value_ \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close> with term antiquotations,
for instance \<^theory_text>\<open>@{value_ \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close>
will print the value of the \<^const>\<open>mcc\<close> attribute of the instance \<open>FT\<close>.
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator but this
argument must be specified after a default optional argument already defined
by the text antiquotation implementation.
So one must use the following syntax if he does not want to specify the first optional argument:
\<open>@{value_ [] [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>. Note the empty brackets.
\<close>
(*<*)