Re: [isabelle] Linear Ordering for nat list



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. 

-- 
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.






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