The Coq mailing list

[Peng Wang <wangp.thu AT gmail.com>]

Thanks for all the help! I think the "alias definition + type annotation" approach suggested by Beta and Pierre-Yves will do the trick. I may file a feature request in the future.

Best,

Peng (Perry) Wang

On Mon, Jun 23, 2014 at 10:37 AM, Strub, Pierre-Yves <pierre-yves AT strub.nu> wrote:

Hi,

One way to work around this is to define your canonical structure on an alias of your type. See for example the left-module canonical structure for rings when these last are acting on themselves (Search for the notation "R ^o" in ssralg.v). You then have to give some type annotation, e.g.:

  Goal forall (R : ringType) (x y : {poly R}^o), x *: y = x * y.

choose the wanted lmodule structure for {poly R}. Note that R^o is convertible to R.

Best,
-- Pierre-Yves.

On 2014-06-18 00:56, Peng Wang wrote:

Is there a way to remove or update a canonical structure registration?

For example, SSReflect's matrix.v registers a canonical structure
matrix_lmodType to declare that ring-element matrices form an L-module
whose scalars are of the same type as the elements. But for
algebra-element matrices, there is another way to form an L-module,
where scalars are from the underlying ring of the algebra. I want to
register this alternative L-module structure to be canonical (e.g. to
talk about "a matrix of functions scaled by a constant"), but Coq's
Canonical Structure command only respects the first registration and
ignores later ones.

--
Peng Wang (王鹏)

CSAIL, The Stata Center, MIT

77 Massachusetts Ave, 32-G822

Cambridge, MA 02139

Phone: (617)803-2025

Email: wangpeng AT csail.mit.edu