Stream: Coq devs & plugin devs

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


view this post on Zulip 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: Oct 15 2021 at 19:03 UTC