Re: [isabelle] Specializing types in locales

Hi Andreas,

Your approach with for would work nicely if it did not erase all mixfix syntax annotations on the parameters.

Sorry, I had misread your message.

The syntax of a *parameter* is either given in a fixes element or a for clause. If no syntax is specified, this means that no syntax is requested. This is so even in a for clause, because there needs to be a mechanism to get rid of unwanted syntax when extending a locale.

While replying I though of the syntax of a *constant* (as introduced by a definition statement). Those are preserved under changes of the parameter types.


Yes, it still does, at least with the Isabelle versions I tested: Isabelle repository version 43916ac560a4 and Isabelle 2009-2. Here is a small example:

locale A =
  fixes a :: "'b => 'c" ("%_%")

locale B = A begin
term "%undefined%" -- "works fine"

locale C =
  A a
  for a :: "'b => 'c"
term "%undefined%" -- "Gives inner syntax error at %"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.