Hi, why does this fail?

```
Import GRing.Theory Num.Theory Order.Theory.
Local Open Scope ring_scope.
Lemma test (z : int) : (2 %| `| z |)%N.
set x := (X in `| X |).
```

with `Error: partial term `|_| does not match any subterm of the goal`

I think it's because it's missing the scope annotation. This works:

```
set x := (X in `| X |%N).
```

Thanks!

But I am still a bit confused

Notation ` `| _ | `

is not related to that scope.

In the goal, it is used to disambiguate the divisibility predicate.

It is:

```
From mathcomp Require Import all_ssreflect all_algebra.
Import GRing.Theory Num.Theory Order.Theory.
Local Open Scope ring_scope.
Locate "`| _ |".
(*
Notation "`| m |" := (absz m) : nat_scope
Notation "`| x |" := (Num.Def.normr x) : ring_scope (default interpretation)
*)
Unset Printing Notations.
Lemma test (z : int) : (2 %| `| z |)%N.
(*
z : int
============================
dvdn 2 (absz z)
*)
```

So under `%N`

the notation changes from the default `Num.Def.normr x`

to `absz`

.

You can find this in `ssrint.v`

:

```
Notation "`| m |" := (absz m) : nat_scope.
```

Oh thanks. Sorry for the noise.

I had the very same issue (with a rewrite rule not matching). Too much overloading kills overloading :)

Last updated: Jul 25 2024 at 16:02 UTC