## Stream: new members

### Topic: Why does the following code doesn't type check?

#### Rui Liu (Nov 11 2020 at 23:17):

def f: Π {x : ℕ}, ℕ := fun (x : ℕ), x

def g (f: Π {x : ℕ}, ℕ): ℕ  := f

#check f


It doesn't check for the definition of g, however, since f has implicit argument, I'd assume f has type ℕ. This is also confirmed by #check f will print ℕ.

#### Reid Barton (Nov 11 2020 at 23:20):

f does have type ℕ but Lean has no way to infer what value to provide for the implicit argument, which is what the error message is complaining about

#### Reid Barton (Nov 11 2020 at 23:21):

for instance, g @f is a term of type ℕ, but what number should it be?

#### Reid Barton (Nov 11 2020 at 23:22):

The function g takes its argument and evaluates it at ...

#### Rui Liu (Nov 12 2020 at 00:11):

OK I see, yeah you're right @Reid Barton

Last updated: May 13 2021 at 04:21 UTC