[isabelle] Making records instances of classes



Hello,

Is it possible to make a record type an instance of a type class?

Here's a simple example of what doesn't work:

record ('a, 'b) Tuple = first :: "'a" second :: "'b"

instance Tuple :: (finite, finite) finite

*** Logical type constructor expected: "t.Tuple"
*** At command "instance" (line 7 of "/tmp/t.thy").

cheers
peter

-- 
http://peteg.org/





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