Ssreflect Users Discussion List

[Vladimir Komendantsky <>]

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