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