Re: [isabelle] Extra type variables in constdef



Hi Nicole,

*** Type unification failed: No type arity itself :: type
*** Type error in application: Incompatible operand type
[..]
What is wrong here? Is there any way to add extra type variables to the set specification?

You need to declare somewhere:

arities itself :: (type) type

This probably should be done in HOL.thy in the distribution already, but currently isn't.

Cheers,
Gerwin





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