implicit arguments

Stream: general

[petercommand]

Is there any way to tell lean to show all the implicit arguments in an error message?
For example, sometimes when rewrite fails, I would want to know if there are different implicit args that caused the rewrite to fail

[petercommand]

Or in a type mismatch error

[petercommand]

Sometimes it shows all the implicit arguments sometimes it doesn't

[Johan Commelin]

set_option pp.all true will show you everything... that might be too much though...

[Rob Lewis]

set_option pp.implicit true before the declaration.

[Johan Commelin]

Aah, there you go.

[petercommand]

Thanks

[Rob Lewis]

There are other pp options that autocomplete should show you. all is difficult to read.