Stream: Coq devs & plugin devs

Topic: ✔ Notation declaration datatype


view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:34):

Hi! I'm a bit confused by the terminology: shouldn't this be notation_decl? https://github.com/coq/coq/blob/master/vernac/vernacexpr.ml#L165

Or is it really meant to be a "declaration notation" datatype? What would it mean?

view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:34):

(I'm trying to improve the Metasyntax API with the phase separation, so I really need to get this right because the ADT appears naturally in the interface)

view this post on Zulip Gaëtan Gilbert (Dec 05 2022 at 12:40):

it seems to mean "notation attached to a declaration" judging by the usage (the stuff that goes in where for Fixpoint, Inductive, Record)
also in ppvernac pr_decl_notation unconditionally prints with where

view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:41):

So what's the difference between where_decl_notation (in Metasyntax) and decl_notation?

view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:42):

(I mean the difference in terms of intent, I can read the concrete differences)

view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:43):

Also the information carried by decl_notation does not seem more restrictive than the one for a general notation

view this post on Zulip Maxime Dénès (Dec 05 2022 at 12:53):

Anyway, thanks.

view this post on Zulip Notification Bot (Dec 05 2022 at 12:54):

Maxime Dénès has marked this topic as resolved.


Last updated: Feb 06 2023 at 00:03 UTC