Zulip Chat Archive

Stream: new members

Topic: How, broadly, does Lean infer implicit arguments?


view this post on Zulip Johan Commelin (Jun 08 2020 at 07:05):

@Chris M If f x has type T, and this T already mentions x, then you can replace x by _.

view this post on Zulip Johan Commelin (Jun 08 2020 at 07:05):

Similarly if you have f x hx, and hx mentions x, then you can write f _ hx.

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 07:49):

When I'm coding, if lean is asking for a variable and I know that it can be worked out from what's going on, or even if I think it can, I leave it out on the principle that shorter code is clearer.


Last updated: May 08 2021 at 18:17 UTC