implicit parameters

Stream: new members

[Aniruddh Agarwal]

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

def add {x : ℕ} (y : ℕ) := x + y
#check add    -- add : ℕ → ℕ
#check @add   -- add : Π {x : ℕ}, ℕ → ℕ
#reduce add 2 -- ?M_1.succ.succ

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

[Bryan Gin-ge Chen]

?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]

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

[Bryan Gin-ge Chen]

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.