arguments-are-not-implicit

Stream: general

[Matei Adriel]

I am following along https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html

I tried pasting the following example in neovim: image.png

For some reason, all the arguments have to be explicitly passed for me. Am I doing something wrong?

[Arthur Paulino]

(The #new members stream is better focused on helping with such questions)

What do you mean? What were you expecting to see?

[Matei Adriel]

Arthur Paulino said:

(The #new members stream is better focused on helping with such questions)

What do you mean? What were you expecting to see?

The book says lean should be able to infer what arguments need to be implicit

[Arthur Paulino]

It's easier to see it happening here:

def id' (a : α) := a
#print id'
-- def id'.{u_1} : {α : Sort u_1} → α → α :=
-- fun {α} a => a

Notice how Lean added α as an implicit parameter of id'

In the example that you posted, everything has already been declared to be explicit. Like this:

variable (α : Sort u_1)

def id' (a : α) := a
#print id'
-- def id'.{u_1} : (α : Sort u_1) → α → α :=
-- fun α a => a