Is it to be expected that sometimes
apply_funelim will fail when
funelim will succeed? I have an example where this is the case, but don't know how to minimise yet.
Yes, it might fail because the unification problem is too hard to resolve
Oh ok. I thought
funelim was supposed to be
apply_funelim plus some automation.
It is, in a way. However
funelim makes a goal of the form
forall args, P args (f args) where
P has some equalities to remember the actual arguments of the function, that is trivial to unify with the eliminators conclusion.
apply_funelim does no massaging of the goal in comparison and just launches the (heuristic) higher-order matching in the hope to find a solution.
I see. Thanks. :)
Last updated: May 28 2023 at 18:29 UTC