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!

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.

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: Jun 06 2023 at 23:01 UTC