Ssreflect Users Discussion List

[Georges Gonthier <>]

  The new library has functions mxvec and vec_mx that convert ‘M_(m, n) to ‘rV(m * n) and back. If you absolutely want a list you could also cross abstraction layers, since matrices are represented as finfuns themselves represented as tuples which in turn are represented as lists. So, if A : ‘M_(m, n), then val (val (val A)) is the seq that lists the actual contents of A.

   Note that the new library also has functions that convert row vectors to polynomials and conversely (rVpoly and poly_rV).

 

    Georges

From: Vladimir Komendantsky [mailto:]
Sent: 15 February 2011 15:25
To: ssreflect
Subject: matrix to seq

 

Hello,

Is there a function in ssreflect to sequentialise the contents of a matrix like, for (aT : finType) and (rT : Type),

Definition seq_mx m (M : 'M_(m, #|aT|)) : seq rT :=
  flatten (map (fun i => map (fun j => M i j) (ord_enum #|aT|))
               (ord_enum m)).

To be honest, I haven't proved about this definition much but it seems now that this "flatten" might stand in the way sometime. Is there a standard sequentialisation method?

Is there a better method to convert just a single-row matrix to a list? The above definition is probably too general because I only intend to use it with single-row matrices, that is, where m is 'I_1.

Best regards,
Vladimir