[isabelle-dev] type class instantiation
c-sterna at jaist.ac.jp
Fri Apr 6 07:58:46 CEST 2012
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"
"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).
More information about the isabelle-dev