Stream: Elpi users & devs

Topic: Index syntax


view this post on Zulip Enzo Crance (May 11 2023 at 13:01):

Hello. I would like to understand the :index syntax. Its purpose is to specify which argument the pattern matching is made on first, and IIUC by default it is the first one, right? Suppose I want to index on the third argument, do I write :index (_ _ 1)?

view this post on Zulip Enrico Tassi (May 11 2023 at 18:43):

Yes, but this does not change the order in which arguments are unified. Clauses are first searched through an index to reduce the number of candidates, then these are unified. The index directive changes which argument is used for the first filtering step, not the order followed by unification when clause head and goal are traversed.


Last updated: Oct 13 2024 at 01:02 UTC