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?
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.
I hope you can follow that code, otherwise just ask.
Last updated: Jun 06 2023 at 23:01 UTC