I am struggling with this error:
Flexible term outside pattern fragment: X48 c0 c1 c2 (pglobal (const «...») «...»)
I think it comes from putting variables in a term, then abstracting the term w.r.t. an eigenvariable, then applying the resulting function to a term that is not a variable.
Is there an easy way to remove the non-eigenvariable terms from the scope of the variables? Like an automatic recursive
prune operation that would leave only the visible eigenvariables coming from the traversed binders? The only other options I have found to avoid this problem are:
I think you found the root cause, if
F is an Elpi function over Coq terms and it contains a unification variable and
T is an arbitrary term, then
P = F T is a problematic term, it is outside the pattern fragment.
Now, the easiest way to pass a term like
P to Coq is to use the
@holes! option (it is taken by all APIs taking a term, IIRC).
Another one is to use
coq.elaborate. The former prunes, the latter simply ignores the arguments to the hole.
See https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html#outside-the-pattern-fragment and
Last updated: Jun 06 2023 at 21:01 UTC