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

Reference a bug in polymorphic class implementation

This commit is contained in:
Nicolas Méric 2024-03-04 14:30:58 +01:00
parent 1740898171
commit 42da18cf3a
1 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
View File

@ -693,4 +693,24 @@ lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \<Longrighta
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*)
text\<open>Bug: Checking of text* type against declare_reference is not done.
Should be compatible with type unification mechanism. See the record package\<close>
doc_class 'a AAA_test =
aaa::"'a list"
doc_class 'a BBB_test =
bbb::"'a list"
declare_reference*[aaa_test::"'a::one AAA"]
text\<open>@{AAA (unchecked) \<open>aaa_test\<close>}\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text*[bbb_test::"'a::one BBB"]\<open>\<close>
text*[aaa_test::"int AAA"]\<open>\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text*[aaa_test'::"string AAA"]\<open>\<close>
end