Théo Winterhalter (Dec 24 2020 at 09:50): Théo Winterhalter (Dec 24 2020 at 09:50):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.
Matthieu Sozeau (Jan 04 2021 at 12:41):Yes, it might fail because the unification problem is too hard to resolve
Théo Winterhalter (Jan 04 2021 at 12:49):Oh ok. I thought funelim was supposed to be apply_funelim plus some automation.
Matthieu Sozeau (Jan 04 2021 at 13:11):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.
Théo Winterhalter (Jan 04 2021 at 13:13):I see. Thanks. :)
Last updated: May 28 2023 at 18:29 UTC