nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

advanced example on trace-attribute term-antiquotations

This commit is contained in:
Burkhart Wolff 2022-12-07 16:01:38 +01:00
parent ec0d525426
commit 8cee80d78e
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/tests/Attributes.thy
View File

@ -199,9 +199,15 @@ term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
(* When not commented, should trigger an error:
value*\<open>@{trace-attribute \<open>dfgdfg\<close>}\<close>
*)
value*\<open>(map fst @{trace-attribute \<open>aaa\<close>}) \<close>
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
definition word_test :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is\<^sub>\<longrightarrow>in" 60)
where " w is\<^sub>\<longrightarrow>in rexp \<equiv> DA.accepts (na2da (rexp2na rexp)) (w)"
value* \<open> (map fst @{trace-attribute \<open>aaa\<close>}) is\<^sub>\<longrightarrow>in example_expression \<close>
(*<*)