Zulip Chat Archive
Stream: new members
Topic: See how Lean is inferring arguments?
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?
Kenny Lau (Jun 08 2020 at 06:56):
you can #print the theorem / definition / lemma
Kenny Lau (Jun 08 2020 at 06:56):
with set_option pp.implicit false
Kenny Lau (Jun 08 2020 at 06:56):
(or true, I can't remember)
Chris M (Jun 08 2020 at 06:57):
helpful! thanks!
Last updated: Dec 20 2023 at 11:08 UTC