opt_param

Stream: maths

[Ashvni Narayanan]

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]

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

[Johan Commelin]

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

[Ashvni Narayanan]

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