Stream: Elpi users & devs

Topic: Removing a clause from an Elpi database


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 09 2022 at 13:49):

Your option will the be (also) settable via Set My Option Name ...

view this post on Zulip Enzo Crance (May 09 2022 at 13:50):

Thanks!

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC