On Fri, 6 Apr 2012, Christian Sternagel wrote:
it seems as if a recent change (in the repo version; within the last 2
weeks, but I do not know exactly when) fixed the naming of type
variables inside instantiations.
There are various ongoing reforms (e.g. see changes leading up to
610d9c212376) that address open questions from the last 5 years of local
theory infrastructure. Any unexpected change certainly helps to
understand the situation, and figure out what is right or wrong in the
end.
I have a type "('f, 'v) term" for first-order terms with function
symbols of type "'f" and variables of type "'v" and a type class "show"
that provides a "shows_prec" and a "shows_list" function for efficient
conversion into strings. To instantiate "term" I had (and this actually
worked until recently)
instantiation "term" :: ("show", "show") "show" begin
abbreviation "shows_term t ≡ shows_term' shows shows t"
definition "shows_prec (d::nat) t = shows_term t"
definition "shows_list_term (is::('f::show, 'v::show) term list) =
shows_list_aux shows is"
First, it has required me 1 more minute to parse the above, because it is
indented in such an odd way, with a dangling 'begin'. Isabelle/jEdit will
at some point support a certain text structure (with indentation and
folding etc.), but only in the standard style:
instantiation ...
begin
abbreviation ...
definition ...
end
lemma assoc_term:
"shows_prec d (t::('f::show, 'v::show) term) r @ s = shows_prec d t
(r @ s)"
...
This no longer works and I'm forced to use "'a" and "'b" instead of "'f"
and "'v".
Like the class target, interpretation uses canonical type variable names.
The change of behaviour is a consequence of more precise treatment of the
target context: results are not exported into the bare-bones theory
context as before, and then copied to the target, but exported into the
target directly.
Florian can say, if he originally meant to support different type variable
names as shown above. There might be some type improvement in the context
that needs to be re-adjusted (or some now unused things to be removed).
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
