Ssreflect Users Discussion List

[Guillaume Melquiond <>]

On 15/12/2015 17:34, Nicolas Magaud wrote:
> Dear all,
> 
> I recently started using ssreflect to describe bits and pieces of discrete 
> geometry.
> Some operations I use are represented as matrices and I need to define a 
> function which given a vector $V$, computes $A*V+B$ when $A$ is a square 
> matrix (2x2 or 3x3) and $B$ another vector.
> My matrices are non-empty (n<>0), but the carrier is not a field. However 
> it seems not to be an issue (from what I read in matrix.v).
> 
> I tried and used the notations +m and *m without success. While making 
> experiments, I also faced some issues with \trace and \det which I do not 
> manage to use properly.
> 
> The code I have so far looks like the (simplified) one attached (o.v). I 
> guess this might look like simple questions to most of you. Howerver some 
> assistance in getting started would be appreciated.

If you disable notations, the issue will become much clearer:

The term "M" has type "matrix Z d d" while it is expected to have type
 "matrix (ssralg.GRing.Ring.sort ?12) ?13 ?13".

Basically, you are defining a matrix over the type Z, which does not
have (yet) a ring structure. So you have two ways to fix the issue.
Either you define a ring structure over Z first, or you reuse an
existing type that already has a ring structure. For instance, the "int"
type from ssrint.

Best regards,

Guillaume