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.


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