Stream: Elpi users & devs

Topic: Local context update


view this post on Zulip Enzo Crance (Nov 18 2021 at 14:27):

Hello. I would like a bit more information about the implication => in Elpi. What is the preferred syntax to add several clauses to the context? What is the scope of this arrow? Do I need to use parentheses so that the context is updated for several subsequent goals, or is the context updated until the end of the current declaration (the next final .)?
Thanks.

view this post on Zulip Enrico Tassi (Nov 18 2021 at 14:33):

The precedence of => w.r.t. , is a pitfall: A => (B , C), D here D does not see A, while C does.
To add multiple clauses you can use [C1, C2] => P or (C1, C2) => P. The difference is that the former is easier to synthesize, it's a list for example you can obtain it by std.append. And the list reads C2 => C1 => P while the conjunction reads C1 => C2 => P, recall the last introduced clause takes precedence.


Last updated: Feb 05 2023 at 14:02 UTC