Enzo Crance (May 09 2022 at 13:40): Enzo Crance (May 09 2022 at 13:40):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.
Enrico Tassi (May 09 2022 at 13:47):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.
Enrico Tassi (May 09 2022 at 13:49):Your option will the be (also) settable via Set My Option Name ...
Enzo Crance (May 09 2022 at 13:50):Thanks!
Enrico Tassi (May 09 2022 at 13:50):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
Enzo Crance (May 09 2022 at 13:50):Yeah I hadn't thought about options directly in Coq. Thank you for the reminder
Last updated: Oct 08 2024 at 14:01 UTC