Hi, currently scopes are not propagated beyond a `r.(@p)`

notation, or a bracketed `(@p r)`

:

```
Notation "0" := true : bool_scope.
Axiom f : bool -> bool -> nat.
Check (@f 0) 0. (* Error: second 0 not interpreted in bool_scope *)
Record R := { p : bool -> nat }.
Check fun r => r.(@p) 0. (* Error: 0 not interpreted in bool_scope *)
```

Wouldn't it be more intuitive, since the information is there, to instead propagate the scopes and have the above working? See PR #12685 for comments.

Last updated: Jun 08 2023 at 04:01 UTC