Stream: Coq devs & plugin devs

Topic: Design question: propagating scopes beyond `.(@p)` notation?

Hugo Herbelin (Jul 13 2020 at 08:54):

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: Sep 09 2024 at 05:02 UTC