And here is a version that works for any substructure of (semi)ringType:

```
From elpi.apps Require Import coercion.
#[warnings="-notation-overridden,-ambiguous-paths"]
From mathcomp Require Import all_ssreflect ssralg.
Elpi Accumulate Coercion lp:{{
coercion _ N {{ nat }} Expected Res :-
coq.unify-eq {{ GRing.SemiRing.sort lp:R }} Expected ok, !,
coq.unify-eq {{ GRing.Nmodule.sort lp:V }} Expected ok, !,
Res = {{ @GRing.natmul lp:V (GRing.one lp:R) lp:N }}.
}}.
Elpi Typecheck Coercion.
Section TestNatMul.
Variable R : fieldType.
Variable n : nat.
Check n : R. (* elaborated to n%:R *)
End TestNatMul.
```

should we move this topic to ~~#~~ #Elpi users & devs maybe?**Hierarchy Builder devs & users**

To get this fully usable in MathComp, we still need to figure out the printing part. My current idea is to put a printing only notation in `ring_scope`

that hides `GRing.natmul`

and a printing only notation `%:R`

in a new `ring_coercions`

so that `Enable/Disable Notation : ring_coercions`

can show/hide coercions in the middle of a proof. But any other idea is welcome.

Karl Palmskog said:

should we move this topic to #Hierarchy Builder devs & users maybe?

Maybe in math-comp devs? as it is more linked to MC than HB.

This topic was moved here from #CUDW 2023 > Coercion Hook by Karl Palmskog.

Thanks @Karl Palmskog !

Last updated: Oct 13 2024 at 01:02 UTC