Hi all,
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. To see what I mean:
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"
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". While this is not a severe restriction, I just wanted to know,
whether this change was intentional (and as usual, it's reasons, just
because I'm curious, not because I disagree to the change).
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
