Enzo Crance (Sep 01 2022 at 12:55): Enzo Crance (Sep 01 2022 at 12:55):Hello.
I would like to add a clause to a database in my program, knowing that the program might query the database for this specific clause later. As documented, coq.elpi.accumulate only adds the clause after executing the program, so the program does not find the expected value in the database.
What are my options? Do I need to write external predicates in ML to store these terms in an OCaml hash table, or is there an idiomatic solution in Elpi? Thanks.
Enrico Tassi (Sep 01 2022 at 14:12):Yes, you can use implication. I mean C = predicate arguments, coq.elpi.accumulate .. C, C => code
Enrico Tassi (Sep 01 2022 at 14:12):See the main loop in derive.elpi, I do it like that
Last updated: Oct 13 2024 at 01:02 UTC