Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int



On 02/09/2014 05:28 PM, Gottfried Barrow wrote:
(*NOTE: The "exception TYPE raised" error shown below might be of
interest to someone.)

For example me. Your type definition uses as a raw type a type variable. The new code in lifting that deals with parametricity assumes that the raw type is always a type constructor. I'll take a look at it.

Ondrej




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