Stream: Elpi users & devs

Topic: Map with Coq terms as keys


view this post on Zulip Enzo Crance (Feb 11 2021 at 16:39):

Good afternoon. I think I can use your last example for renaming. However, I will need a map from terms to integers when doing my equivalent of your gen predicate. As creating a map requires a comparison function, is there already a function to compare Coq terms in Elpi somewhere? Thanks!

view this post on Zulip Enrico Tassi (Feb 11 2021 at 16:43):

This one https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi#L307 should work, but as the comment says, it does no like terms with holes.

view this post on Zulip Enrico Tassi (Feb 11 2021 at 16:47):

It should combine well with https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi#L867 but don't expect stellar performances.

IMO once you know exactly how you want your map to behave, we can expose an OCaml data structure, as for https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L1070 which is more efficient since it is implemented entirely in Ocaml.


Last updated: Feb 04 2023 at 02:03 UTC