Johan Commelin (Dec 11 2019 at 09:43):
Can we have a version of
refine that ignores typeclasses. So I write
refine my_lemma _ _ _ _ X _ _ Y, and Lean tries unification. But if it can't find a topology on
X (or whatever) it doesn't complain, but just returns that as a goal.
Johan Commelin (Dec 11 2019 at 09:44):
Currently I just get stupid
max type class errors, and I would like to easily march ahead and break this into subgoals.
Last updated: May 06 2021 at 20:13 UTC