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 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 |
> Programming is just another word for the lost art of thinking.

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