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!
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.
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
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