## Stream: maths

### Topic: opt_param

#### 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 let statement.

#### 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