Ssreflect Users Discussion List

[Vadim Zaliva <>]

Hi!

I am just starting with math-comp and have a couple naive questions:

1. I am in particular interested in Matrix stuff. Are there any examples, presentations, etc. which could help somebody new to ssrelfect and math-comp to get started with it?

2. I have installed coq-mathcomp-algebra opam package under Linux. Should I be concerned about this the following message:

$ coqtop

Welcome to Coq 8.5pl1 (May 2016)

Coq < Require Import mathcomp.algebra.matrix.

Small Scale Reflection version 1.5 loaded.

Copyright 2005-2014 Microsoft Corporation and INRIA.

Distributed under the terms of the CeCILL-B license.

[Loading ML file ssreflect.cmxs ... done]

Small Scale Reflection version 1.5 loaded.

Copyright 2005-2014 Microsoft Corporation and INRIA.

Distributed under the terms of the CeCILL-B license.

[Loading ML file z_syntax_plugin.cmxs ... done]

[Loading ML file quote_plugin.cmxs ... done]

[Loading ML file newring_plugin.cmxs ... done]

Warning: No global reference exists for projection

valuefun

       (x : finfun.finfun_of

              (aT:=fintype.prod_finType

                     (fintype.ordinal_finType _UNBOUND_REL_2)

                     (fintype.ordinal_finType _UNBOUND_REL_1))

              (ssreflect.Phant

                 (fintype.ordinal _UNBOUND_REL_2 *

                  fintype.ordinal _UNBOUND_REL_1 -> _UNBOUND_REL_4)))

       (_ : is_true true) =>

     Matrix (R:=_UNBOUND_REL_5) (m:=_UNBOUND_REL_4) (n:=_UNBOUND_REL_3) x in

instance matrix_subType of eqtype.Sub, ignoring it.

Coq <   

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060