Zulip Chat Archive

Stream: general

Topic: implicit arguments


view this post on Zulip 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

view this post on Zulip petercommand (Jan 10 2019 at 08:44):

Or in a type mismatch error

view this post on Zulip petercommand (Jan 10 2019 at 08:44):

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

view this post on Zulip Johan Commelin (Jan 10 2019 at 08:44):

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

view this post on Zulip Rob Lewis (Jan 10 2019 at 08:44):

set_option pp.implicit true before the declaration.

view this post on Zulip Johan Commelin (Jan 10 2019 at 08:44):

Aah, there you go.

view this post on Zulip petercommand (Jan 10 2019 at 08:44):

Thanks

view this post on Zulip 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