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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and