Stream: Coq devs & plugin devs

Topic: When to group vernac command extend?


view this post on Zulip Li-yao (Apr 09 2022 at 19:00):

In a .mlg, what's the difference between having multiple VERNAC COMMAND EXTEND vs a single one? And what's the purpose of the name after EXTEND?

VERNAC COMMAND EXTEND ...
| [ "FOO" ] -> { ... }
| [ "BAR" ] -> { ... }
END

(* vs *)


VERNAC COMMAND EXTEND ...
| [ "FOO" ] -> { ... }
END

VERNAC COMMAND EXTEND ...
| [ "BAR" ] -> { ... }
END

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2022 at 19:07):

This changes the factorization rules of the parsing engine

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2022 at 19:07):

If your command are discriminated by their first entry it will be equivalent

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2022 at 19:08):

(there is more factorization going on with the first variant)

view this post on Zulip Gaëtan Gilbert (Apr 09 2022 at 21:55):

what about the name?


Last updated: Feb 02 2023 at 13:03 UTC