Zulip Chat Archive

Stream: new members

Topic: See how Lean is inferring arguments?


view this post on Zulip Chris M (Jun 08 2020 at 06:51):

Is there a way to see which arguments lean is inferring, when using a term with implicit arguments?

view this post on Zulip Kenny Lau (Jun 08 2020 at 06:56):

you can #print the theorem / definition / lemma

view this post on Zulip Kenny Lau (Jun 08 2020 at 06:56):

with set_option pp.implicit false

view this post on Zulip Kenny Lau (Jun 08 2020 at 06:56):

(or true, I can't remember)

view this post on Zulip Chris M (Jun 08 2020 at 06:57):

helpful! thanks!


Last updated: May 14 2021 at 22:15 UTC