Zulip Chat Archive

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 : ℕ → ℕ
#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 (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: Dec 20 2023 at 11:08 UTC