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

Update bug declare_reference* bug example

This commit is contained in:
Nicolas Méric 2024-03-11 15:51:34 +01:00
parent 46b094939a
commit a1677384b3
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -704,12 +704,15 @@ bbb::"'a list"
declare_reference*[aaa_test::"'a::one AAA_test"]
text\<open>@{AAA_test (unchecked) \<open>aaa_test\<close>}\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text*[bbb_test::"'a::one BBB_test"]\<open>\<close>
text\<open>aaa_test should fail and trigger an error because its type was \<^typ>\<open>'a::one AAA_test\<close>
in the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
(*text*[aaa_test::"'a::one BBB_test"]\<open>\<close>*)
text*[aaa_test::"int AAA_test"]\<open>\<close>
text\<open>bbb_test should fails and trigger an error \<close>
text\<open>aaa_test' should fail and trigger an error because its type \<^typ>\<open>string AAA_test\<close>
is not compatible with its type \<^typ>\<open>'a::one AAA_test\<close> declared in
the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
text*[aaa_test'::"string AAA_test"]\<open>\<close>