I want 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? Should I write external predicates in ML to store these terms in an OCaml hash table, or is there an idiomatic solution in Elpi? Thanks.
Yes, you can use implication. I mean
C = predicate arguments, coq.elpi.accumulate .. C, C => code
See the main loop in
derive.elpi, I do it like that
Last updated: Feb 05 2023 at 14:02 UTC