Enzo Crance (Feb 18 2021 at 19:33): Enzo Crance (Feb 18 2021 at 19:33):Is there a way to apply a rewrite lemma in elpi? If not, I have a backup solution to express it that requires to be able to beta-expand any term containing one or more occurrences of a value v into some P v. Is there a way to find that P in elpi?
Enrico Tassi (Feb 18 2021 at 20:03):beta-expanding, as you call it, it's easy to do in elpi. It's a key component of HO unification, and elpi was meant for that. This piece of code from an (experimental) elaborator for Coq does that for a list of terms, not just one. https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-elaborator.elpi#L159 It's like "copy" but goes the other way.
There is a big question mark, that is "how do you compare a term with v" and what the code I wrote does is to use keyd-matching, a concept from ssreflect also use in the HO unification of matita. Depending on your user case you may want to change that.
Enrico Tassi (Feb 18 2021 at 20:04):I hope you can follow that code, otherwise just ask.
Last updated: Apr 19 2024 at 22:01 UTC