Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Antiquotation causes type check errors elsewhere

Email Gateway (Feb 23 2022 at 11:44):

From: Stefan Haan <stefan.haan@aau.at>
As discussed in the #isabelle IRC channel:
Following Isabelle code causes an Bad number of arguments for type constructor: "Test.R" error at the "x" definition:

record ('a, 'b) R =
  field :: nat

locale L =
  fixes r :: "('a, 'b) R"
begin
  definition "x ≡ 42"
   ― ‹ here something about \<^typ>‹R› is wrong›
end

I found this quite confusing as type R is never used in the
definition of x. But clearly something is wrong with it, so let's
delete the x definition line. Surprisingly, this causes the error to
jump further up to the locale declaration. This also confused me
because:

1) I assumed the code to be correct until the definition line.

2) Clearly I used the right number of type arguments in fixes r.

It took me a while to realize that the problem was the typ
antiquotation in the comment below the x definition. I think the error
should have been shown on the antiquotation.

Best greetings,
Stefan Haan
Test.thy
smime.p7s

Last updated: Jul 15 2022 at 23:21 UTC