## Stream: new members

### Topic: implicit parameters

#### Aniruddh Agarwal (May 17 2020 at 01:59):

I performed a little experiment in an attempt to understand implicit arguments:

def add {x : ℕ} (y : ℕ) := x + y
#check @add   -- add : Π {x : ℕ}, ℕ → ℕ


I'm not sure how to interpret the result of #reduce add 2.

#### Bryan Gin-ge Chen (May 17 2020 at 02:01):

?M_1 is a metavariable. In this case it stands for a nat which hasn't been specified yet. The pretty printer is using dot notation, so recall that n.succ for n : nat is the same as nat.succ n.

#### Aniruddh Agarwal (May 17 2020 at 02:06):

Can I somehow substitute ?M_1 to get an actual natural out?

#### Bryan Gin-ge Chen (May 17 2020 at 02:08):

No, I think you have to use @ to supply a value for x. In general, arguments which can't be inferred from later arguments shouldn't be made implicit.

Last updated: May 14 2021 at 14:20 UTC