## Stream: new members

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

#### 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 _.

#### 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.

#### 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