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



On 02/09/2014 11:40 PM, Ondřej Kunčar wrote:
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

The problem is addressed in 6ea67a791108.

Just a side note: I am not sure if linordered_idom is the best choice because I fear you cannot prove that your type 'a loidN is again in linordered_idom (usual problems with minus). Which I believe, you would like to do.

Best,
Ondrej




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