Re: [isabelle] Linear Ordering for nat list

On 02/05/2012, at 9:48 AM, Aaron W. Hsu wrote:

> On Wed, 02 May 2012 00:03:07 +0100, John Wickerson wrote:
>> I reckon this is a job for isabelle's "type classes". You should make an
>> instantiation of the "linorder" class (defined in
>> for nat lists.
> Thank you!  I have not used type classes before, but after reading about 
> them, I think I can make it work. 

Before you do, have a poke around the Isabelle sources. There are a few theories about list orders already in there (e.g. "Length Lexicographic Ordering" in src/HOL/List.thy and probably a prefix order somewhere).



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