Definition with implicit types

Stream: new members

[Ken Roe]

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]

What error do you get?

[Simon Hudon]

Also, can you enclose your code between three ticks:

```lean
-- your code here
```

[Chris Hughes]

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]

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

[Kenny Lau]

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

[Chris Hughes]

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

[Chris Hughes]

If you were to put the Types after the colon.

[Chris Hughes]

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

[Ken Roe]

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]

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

[Mario Carneiro]

after the definition

[Ken Roe]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

resulting in errors which completely throw the user