Julio Di Egidio (Oct 10 2023 at 14:31): Julio Di Egidio (Oct 10 2023 at 14:31):Hi there, I have been reading about Elpi, so far my understanding (still very limited) being that I can use Elpi to define tactics that construct/elaborate proof terms: anyway, in particular, I seem unable to find/understand what happens with non-deterministic facts or rules. (Apologies if the question is too basic: I have been reading, not fully yet, through the suggested papers, maybe I am missing something obvious.)
Enrico Tassi (Oct 10 2023 at 14:39):Rules are given an operational meaning following SLD resolution (they are tried in order, and if there is a failure it bracktracks).
There is a very simple example here, see the blind tactic.
In that case the rules are clearly non deterministic, they have the very same head, but give different results.
Julio Di Egidio (Oct 10 2023 at 14:55):Ah, I think I see: "relates one goal to a list of subgoals", meaning that we get a new goal for each possible result, as indeed tactics do...! Thanks very much: also I am finding that tutorial very helpful.
Enrico Tassi (Oct 10 2023 at 14:57):The coq-elpi page on github has a few of these, feedback is welcome
Notification Bot (Oct 10 2023 at 14:57):Enrico Tassi has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC