Zulip Chat Archive

Stream: general

Topic: refine and type class inference


view this post on Zulip 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.

view this post on Zulip 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