Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hello and welcome!

 

For initial material, you may want to look into the Advanced Coq Winter School course material; lesson 7 covers the matrix library (but you’ll need much of the earlier material as well).

 

You don’t need to worry about this type of warning (no global reference exists for projection value) in the library; you should however investigate should you get it in your own development (it has to do with unification hints for canonical structure instances – if you don’t know what these are don’t worry). There are many other kinds of spurious warnings triggered by the library, in particular Notation overriding and redundant Coercion paths, which you should all ignore. Unfortunately Coq does not let us selectively turn these off.

 

     Best,

Georges

 

From: [mailto:] On Behalf Of Vadim Zaliva
Sent: 18 May 2016 21:13
To:
Subject: [ssreflect] math-comp examples, import warning

 

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