[isabelle] Extra type variables in constdef



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.