Janno (Jan 19 2021 at 16:01): Janno (Jan 19 2021 at 16:01):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.
Matthieu Sozeau (Jan 19 2021 at 19:13):It should I guess, just beware of the type being reduced too
Janno (Jan 20 2021 at 09:54):Interesting point about the type. Luckily the type in my example is super simple and both x and 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 [...] ?
Janno (Jan 21 2021 at 12:54):Just the context of the goal. No more output from Set Debug Tactic Unification.
Matthieu Sozeau (Jan 21 2021 at 13:20):Then that's a bug I guess :)
Last updated: Oct 13 2024 at 01:02 UTC