Consider the following example:

```
Variables (A B : Type) (B_of_A : A -> B).
Coercion B_of_A : A >-> B.
Goal forall (a : A), a = a :> B.
(*
============================
forall a : A, a = a
*)
```

Why does the `:> B`

disappear? Sanity check:

```
Set Printing Coercions.
(*
============================
forall a : A, B_of_A a = B_of_A a
*)
Unset Printing Coercions.
Abort.
```

so the coercion is there.

In the following example the `:>`

doesn't disappear:

```
From mathcomp Require Import ssrint.
Open Scope ring_scope.
Goal forall (n : nat), n = n :> int.
(*
============================
forall n : nat, n = n :> int
*)
```

However now a different strange thing happens: `Set Printing Coercions`

doesn't do anything:

```
Set Printing Coercions.
(*
============================
forall n : nat, n = n :> int
*)
Unset Printing Notations.
(*
============================
forall n : nat, eq (Posz n) (Posz n)
*)
Abort.
```

Is any of this behaviors possibly a bug?

`_ = _ :> _`

is a notation

don't know what mathcomp does

It's not a bug. There can be more than one notation for the same expression, and when printing, one notation has to be chosen.

Sure, but why does the choice change in these two examples? Or do you think that mathcomp redefines the notation? Shouldn't the supposed redefinition also change the behavior of the `B_of_A`

example? (It doesn't change if done after importing mathcomp stuff).

In mathcomp, in order to disambiguate `n = m :> nat`

and `n = m :> int`

when `n`

and `m`

are in `nat`

and a coercion to `int`

is potentially triggered, we force the printing of the ternary form explicitly:

https://github.com/math-comp/math-comp/blob/bd9431c4926e10c39da8a20374dd2050120fab32/mathcomp/algebra/ssrint.v#L70

(the `'in' 't'`

hack comes from the time it was not possible to register several printing rules for the same notation format in Coq, so we use a combination of two strings `in`

and `t`

that render to `int`

when glued together at printing time, you can ignore this hack, which we should replace by now-legitimate Coq code, I believe)

Ok, I admit I did not see that coming, thanks.

Why `'in' 't'`

instead of `'int'`

?

Ana de Almeida Borges said:

Why

`'in' 't'`

instead of`'int'`

?

see my previous message.

So we couldn't have `int`

as both a token in a notation and the name of a type?

to be clearer regarding `a = a :> B`

: that disappears because that’s just a notation for `@eq B a a`

, unlike the math-comp notations (and I’d expect it to be a parsing-only notation).

Ana de Almeida Borges said:

So we couldn't have

`int`

as both a token in a notation and the name of a type?

No, that's a different problem, Coq would not make it a token. It's just the left over of a missing feature that has been added since then.

I removed it in math-comp/math-comp#834

Last updated: May 24 2024 at 22:02 UTC