Ali Caglayan (Aug 02 2021 at 14:49): 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
Ali Caglayan (Aug 02 2021 at 14:49):Should we probably separate Equality into it's own command?
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.
Ali Caglayan (Aug 03 2021 at 15:29):I had a go at this here: https://github.com/coq/coq/pull/14740
Ali Caglayan (Aug 03 2021 at 15:29):However I am having some issues with the parser and Equality
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?
Ali Caglayan (Aug 03 2021 at 15:33): Ali Caglayan (Aug 03 2021 at 15:33):I have very little idea what I am doing here 0:-)
Hugo Herbelin (Aug 04 2021 at 09:35):Ali Caglayan said:
how can I tell the parser to only treat
Equalityas a keyword when it followsScheme?
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)?
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.
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: Dec 01 2023 at 06:01 UTC