Zulip Chat Archive

Stream: maths

Topic: opt_param


view this post on Zulip Ashvni Narayanan (Dec 17 2020 at 09:20):

I am using the following function as a condition in a lemma :

(g :    := λ i, if i = 0 then 0 else (1 / (nat.factorial (i) )) )

Lean changes this to :

g: opt_param (  ) (λ (i : ), ite (i = 0) 0 (1 / (i.factorial)))

I don't know what opt_param is, or why it appears there, or how to work with it. The only option I see is apply_opt_param, but that does not help.

Any help is appreciated, thank you!

view this post on Zulip Johan Commelin (Dec 17 2020 at 09:25):

Lean thinks that you want a variable g with a default argument.
But that's not what you meant.

view this post on Zulip Johan Commelin (Dec 17 2020 at 09:26):

So, it's probably the easiest to turn g into a separate definition. Although you could also use a let statement.

view this post on Zulip Ashvni Narayanan (Dec 17 2020 at 09:27):

Ah I see. Yes I did that, it works! Thank you!


Last updated: May 10 2021 at 07:15 UTC