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

Fix typo

This commit is contained in:
Nicolas Méric 2024-03-12 16:02:25 +01:00
parent a1677384b3
commit 10b98b660f
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -693,7 +693,7 @@ 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.
text\<open>Bug: Checking of \<^theory_text>\<open>text*\<close> type against \<^theory_text>\<open>declare_reference*\<close> is not done.
Should be compatible with type unification mechanism. See the record package\<close>
doc_class 'a AAA_test =
aaa::"'a list"
@ -704,13 +704,13 @@ bbb::"'a list"
declare_reference*[aaa_test::"'a::one AAA_test"]
text\<open>@{AAA_test (unchecked) \<open>aaa_test\<close>}\<close>
text\<open>aaa_test should fail and trigger an error because its type was \<^typ>\<open>'a::one AAA_test\<close>
text\<open>\<open>aaa_test\<close> 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>aaa_test' should fail and trigger an error because its type \<^typ>\<open>string AAA_test\<close>
text\<open>\<open>aaa_test'\<close> 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>