make explicit argument implicit

Stream: general

[Zesen Qian]

Hi, is it possible to temprorarily make an argument implicit? Say, instead of id bool true, I write something like id _ true and let the elaborator to infer the omitted argument for me. (id : \forall A, A -> A is completely explicit)

[Zesen Qian]

funny, seems lean can already do it exactly like I demonstrated. never knew that.

[Reid Barton]

You can already write id _ true and the elaborator will infer the argument (though true is a Prop, not a bool).
Did you have something else in mind?

[Reid Barton]

Ah, okay.

[Reid Barton]

A useful trick with this is also to define a notation local notation `id'` := id _ if you want to make an argument implicit in an entire file/section of code.

[Zesen Qian]

@Reid Barton good, thanks.