Enzo Crance (Feb 11 2021 at 16:39): 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!
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.
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: Apr 19 2024 at 02:02 UTC