Re: [isabelle] Extra type variables in constdef
This is a well-known problem with type classes. The point is that your c
might depend on the choice of the intermediate 'a. One way around this
is to annotate "b (a x)" with some specific type.
Nicole Rauch wrote:
I'm having trouble getting rid of extra type variables that appear on
the right-hand side of a constant definition. This is my setting:
axclass someAxClass < type
a :: "int => ('a::someAxClass)"
b :: "('a::someAxClass) => bool"
Now if I define a constant that groups together these two consts, say
c :: "int => bool"
"c x == b (a x)"
I get the error message
*** Specification depends on extra type variables: "'a"
Is there any way to work around this, e.g. can c depend on 'a (similar
to polymorphic datatype declarations) ?
Or is my attempt generally considered bad design and should be
Thanks for any insights
This archive was generated by a fusion of
Pipermail (Mailman edition) and