Stream: new members

Topic: Definition with implicit types

Ken Roe (Jul 10 2018 at 22:17):

Can someone correct the syntax for this definition:

def bind_option : {Π X : Type}, {Π Y : Type},
option X → (X → option Y)
→ option Y
| option.none f := @option.none Y
| (option.some x) f := f x

Simon Hudon (Jul 10 2018 at 22:21):

What error do you get?

Simon Hudon (Jul 10 2018 at 22:22):

Also, can you enclose your code between three ticks:

lean



Chris Hughes (Jul 10 2018 at 22:22):

def bind_option {X : Type} {Y : Type} :
option X → (X → option Y)
→ option Y
| option.none f := @option.none Y
| (option.some x) f := f x


Chris Hughes (Jul 10 2018 at 22:23):

pattern matching is done on everything after the colon, which is why is moved the Types before the colon.

Kenny Lau (Jul 10 2018 at 22:23):

def bind_option {X : Type} {Y : Type} :
option X → (X → option Y)
→ option Y
| none f := none
| (some x) f := f x


Chris Hughes (Jul 10 2018 at 22:24):

Also Pi should be out of the brackets like this  Π {X Y : Type},

Chris Hughes (Jul 10 2018 at 22:24):

If you were to put the Types after the colon.

Chris Hughes (Jul 10 2018 at 22:24):

Incidentally this function exists in the library and it's called option.bind I think

Ken Roe (Jul 10 2018 at 22:36):

Not quite--I get the following error on the "f x" term of the last line:

function expected at
f x
term has type
option Y

Mario Carneiro (Jul 10 2018 at 22:40):

perhaps you have something on the following line(s)?

Mario Carneiro (Jul 10 2018 at 22:40):

after the definition

Ken Roe (Jul 10 2018 at 22:49):

This was the problem. The error goes away if I add a period.

Mario Carneiro (Jul 10 2018 at 22:51):

Usually we fix this by just having the next line start with some kind of command like def, namespace, or a comment. Presumably that line is giving you an error anyway otherwise

Kenny Lau (Jul 10 2018 at 22:51):

what can there be after that thing? I think all my lines start with keywords

Sebastian Ullrich (Jul 11 2018 at 07:20):

Btw, we're thinking of not allowing function applications to stretch over empty lines in Lean 4 to fix such issues. I do hope that would not break anyone's weird code...?

Kevin Buzzard (Jul 11 2018 at 07:36):

I see newbie errors like this all the time (I'm currently teaching Lean to a bunch of people)

Kevin Buzzard (Jul 11 2018 at 07:37):

the function expects one or two more values so it just starts eating into the next command

Kevin Buzzard (Jul 11 2018 at 07:37):

resulting in errors which completely throw the user

Last updated: May 14 2021 at 07:19 UTC