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
Should we probably separate Equality
into it's own command?
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.
I had a go at this here: https://github.com/coq/coq/pull/14740
However I am having some issues with the parser and Equality
how can I tell the parser to only treat Equality
as a keyword when it follows Scheme
?
I have very little idea what I am doing here 0:-)
Ali Caglayan said:
how can I tell the parser to only treat
Equality
as 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)?
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.
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: Jun 09 2023 at 07:01 UTC