If I copy the output of
Set Debug Cbv on
let x := eval cbv in y in assert (x = y), convert all
Unfolding <constant> lines into
Hint Transparent <constant> : my_db, and then try to solve the goal (
x = y) with
autoapply @eq_refl with my_db, should I expect this to succeed? It doesn't solve the goal in my local example but I don't have anything minimized yet and wanted to check if my assumptions make any sense.
It should I guess, just beware of the type being reduced too
Interesting point about the type. Luckily the type in my example is super simple and both
y have the same type even without any reduction. As far as I can tell, tactic unification in
autoapply (@eq_refl my_type x) with my_db fails on the terms itself but it doesn't give me any useful information:
Debug: Starting unification Debug: Leaving unification with failure [...] Unable to unify "x = x" with "x = y"
What's in the [...] ?
Just the context of the goal. No more output from
Set Debug Tactic Unification.
Then that's a bug I guess :)
Last updated: Sep 25 2023 at 14:01 UTC