Re: [isabelle] Linear Ordering for nat list



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. 

On 1 May 2012, at 22:26, Aaron W. Hsu wrote:

> I want to do something like "Max {[0,1],[1,0]}" but I think that I need 
> to somehow define a linear ordering on "nat list", am I right?  Is there 
> somewhere that I can read about how to do this?
> 
> -- 
> 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.