Hello. Does the opposite of
coq.elpi.accumulate exist? That is, is it possible to remove a clause previously added to a database? I am thinking about this feature to make a command to set and unset a flag, and the flag would be represented with a predicate stored in a database.
I think you want to use this: https://github.com/LPCIC/coq-elpi/blob/2a511a7edb9ebecad52f094111abd9c0c4187f7c/coq-builtin.elpi#L1247
You cannot remove a clause, but you can accumulate one before it, and kill it with cut. But that is not what you need to do here.
Your option will the be (also) settable via
Set My Option Name ...
It is really a Coq option, it is just that you declare it in Elpi. Of course you can also read/write already exisinting options
Yeah I hadn't thought about options directly in Coq. Thank you for the reminder
Last updated: Jun 06 2023 at 22:01 UTC