Zulip Chat Archive

Stream: general

Topic: refine and type class inference

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: Aug 03 2023 at 10:10 UTC