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.

Tobias

Nicole Rauch wrote:
Dear all,

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

consts
a :: "int => ('a::someAxClass)"
b :: "('a::someAxClass) => bool"

Now if I define a constant that groups together these two consts, say

constdefs
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 formalized differently?

Thanks for any insights

Nicole Rauch





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