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