Re: [isabelle] reasoning about classes of many-sorted structures

On Friday 20 February 2009 12:23:17 Andrei Popescu wrote:
> As far as I see, type classes do not allow multiple type
> variables.  Concretely, say I
> want to reason about vector spaces (K,V,+,*,...)  without having either of
> K and V fixed.  Is there any elegant way around this?   

Have you looked at using locales? I'm just learning about them myself at the 
moment, and all the examples I've seen in the documentation use only one type 
variable, but I don't immediately see why locales wouldn't work with more than 
one type variable.


Attachment: signature.asc
Description: This is a digitally signed message part.

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