Stream: Coq devs & plugin devs

Topic: Intended semantics of `Scheme` command


view this post on Zulip Ali Caglayan (Aug 02 2021 at 14:49):

What are the intended semantics of the Scheme command? The Equality scheme_kind seems to be problematic. The identifier syntax is broken for example: https://github.com/coq/coq/issues/14735

view this post on Zulip Ali Caglayan (Aug 02 2021 at 14:49):

Should we probably separate Equality into it's own command?

view this post on Zulip Ali Caglayan (Aug 02 2021 at 14:54):

The with _ := _ syntax with Equality also doesn't really make sense and gives a warning like Unexpected error during scheme creation: Automatic building of boolean->Leibniz lemmas not supported which isn't very useful.

view this post on Zulip Ali Caglayan (Aug 03 2021 at 15:29):

I had a go at this here: https://github.com/coq/coq/pull/14740

view this post on Zulip Ali Caglayan (Aug 03 2021 at 15:29):

However I am having some issues with the parser and Equality

view this post on Zulip Ali Caglayan (Aug 03 2021 at 15:30):

how can I tell the parser to only treat Equality as a keyword when it follows Scheme?

view this post on Zulip Ali Caglayan (Aug 03 2021 at 15:33):

https://github.com/coq/coq/pull/14740/files#diff-7a77660cab5c23a4ec78a2c6726d6808e90d7dfb364098ece99d13920e23648bR239

view this post on Zulip Ali Caglayan (Aug 03 2021 at 15:33):

I have very little idea what I am doing here 0:-)

view this post on Zulip Hugo Herbelin (Aug 04 2021 at 09:35):

Ali Caglayan said:

how can I tell the parser to only treat Equality as a keyword when it follows Scheme?

Isn't the rule IDENT "Scheme"; IDENT "Equality" working as expected (i.e. taking precedence on IDENT "Scheme"; l = LIST1 scheme SEP "with" whenever possible)?

view this post on Zulip Ali Caglayan (Aug 04 2021 at 10:12):

OK, looks like I've done that correctly then. Before I had IDENT "Scheme"; "Equality" however this was failing with Class Equality := .... I changed it to the one you said, but I am not really sure what the difference is.

view this post on Zulip Théo Zimmermann (Aug 05 2021 at 05:03):

The difference is that putting IDENT avoids declaring a new keyword. Once you insert a new keyword, you break any use of the corresponding identifier. But you don't need a new keyword to introduce a new command.


Last updated: Oct 21 2021 at 20:02 UTC