## Stream: general

### Topic: implicit arguments

#### petercommand (Jan 10 2019 at 08:43):

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 (Jan 10 2019 at 08:44):

Or in a type mismatch error

#### petercommand (Jan 10 2019 at 08:44):

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

#### Johan Commelin (Jan 10 2019 at 08:44):

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

#### Rob Lewis (Jan 10 2019 at 08:44):

set_option pp.implicit true before the declaration.

#### Johan Commelin (Jan 10 2019 at 08:44):

Aah, there you go.

Thanks

#### Rob Lewis (Jan 10 2019 at 08:44):

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

Last updated: May 10 2021 at 00:31 UTC