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
>> http://isabelle.in.tum.de/library/HOL/Orderings.html) 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