[isabelle] matrix constructions
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] matrix constructions
- From: Viorel Preoteasa <viorel.preoteasa at abo.fi>
- Date: Thu, 31 Mar 2011 17:56:32 +0300
- User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:22.214.171.124) Gecko/20110303 Lightning/1.0b2 Thunderbird/3.1.9
I have a class that has the binary operations * and +, and I would like
an instantiation of this class for matrices with the usual operations
(A * B) i j = Sum_k (A i k) * (B k j).
The dimension of the matrices must be finite because the plus operation
Is there a way of defining this structure with the instantiation
mechanism of Isabelle?
This archive was generated by a fusion of
Pipermail (Mailman edition) and