Zulip Chat Archive

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