Add basic explanation for lemma*, etc.
ci/woodpecker/push/build Pipeline failed
Details
ci/woodpecker/push/build Pipeline failed
Details
Add basic explanation how to use lemma*, etc. with term antiquotations of polymorphic class instances
This commit is contained in:
parent
8d6c8929e2
commit
43aad517b9
|
@ -679,4 +679,13 @@ typ\<open>unit test_G_ext\<close>
|
||||||
typ\<open>\<lparr>test_G.tag_attribute :: int\<rparr>\<close>
|
typ\<open>\<lparr>test_G.tag_attribute :: int\<rparr>\<close>
|
||||||
text*[xcv6::"\<lparr>test_G.tag_attribute :: int\<rparr> test_F", b="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"]\<open>\<close>
|
text*[xcv6::"\<lparr>test_G.tag_attribute :: int\<rparr> test_F", b="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"]\<open>\<close>
|
||||||
|
|
||||||
|
|
||||||
|
text\<open>\<open>lemma*\<close>, etc. do not support well polymorphic classes.
|
||||||
|
For now only embedded term-antiquotation in a definition could work:\<close>
|
||||||
|
definition* testtest_level where "testtest_level \<equiv> the (text_section.level @{test2 \<open>testtest2''\<close>})"
|
||||||
|
lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \<Longrightarrow> xx = yy" by simp
|
||||||
|
|
||||||
|
text\<open>Indeed this fails:\<close>
|
||||||
|
(*lemma*[e6::E] testtest : "xx + the (level @{test2 \<open>testtest2''\<close>}) = yy + the (level @{test2 \<open>testtest2''\<close>}) \<Longrightarrow> xx = yy" by simp*)
|
||||||
|
|
||||||
end
|
end
|
Loading…
Reference in New Issue