Added new CEP Symbol Sets #84
Conversation
|
|
||
| A possible syntax would be: | ||
| - Command **Declare Symbol Set** *ident* **:=** *symbol_set_expr* | ||
| - *symbol_set_expr* ::= **Module** *qualid* | **Module Recursive** *qualid* | *reference* | *symbol_set_expr* [**+ * -**] *symbol_set_expr* | **(** *symbol_set_expr* **)** |
There was a problem hiding this comment.
what if someone does Definition Module := ... or Module Recursive. End Recursive.?
I wouldn't be shocked if the second one actually exists somewhere.
There was a problem hiding this comment.
Indeed the syntax is not very well thought through - mostly because I know little about how such "global syntax" messes with the parser and notation system. IMHO designing good Coq syntax is an art on its own, which I would prefer to leave to those who understand it.
|
See also coq/coq#6144 |
|
Maybe lists of constants could (indeed) be assembled into "unfolding hints" and various set-theoretic operations could apply more generally to all kinds of hint databases, including providing automatic inclusion of all constants from a module? |
|
@herbelin : indeed allowing set operations on auto hint databases would also be a very useful feature. If one can find a common syntax to handle "unfolding databases" and hint databases, I would appreciate it. But please note that it should be possible to collect all symbols of a module without touching the module itself, say starting some auto collection. |
No description provided.