Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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 .

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 11 2020 at 23:21):

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

view this post on Zulip Reid Barton (Nov 11 2020 at 23:22):

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

view this post on Zulip 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