Zulip Chat Archive

Stream: lean4

Topic: reducible instances


view this post on Zulip Jason Gross (Mar 19 2021 at 14:29):

Is there a way to get the failed to synthesize instance message to print after all the inline/reducible things have been unfolded?

view this post on Zulip Mario Carneiro (Mar 19 2021 at 21:39):

I don't think that's how it works. Typeclass inference unfolds reducibles while attempting to unify the typeclass subgoal with an instance, it doesn't do a two pass thing where it first eagerly unfolds reducibles then does typeclass inference

view this post on Zulip Mario Carneiro (Mar 19 2021 at 21:40):

Probably if you want this behavior it would be an explicit thing, i.e. you could do apply_instance <|> dsimp reducible >> fail "failed to synthesize instance" or whatever the lean 4 equivalent of that is


Last updated: May 07 2021 at 13:21 UTC