Zulip Chat Archive

Stream: new members

Topic: Definition with implicit types


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

view this post on Zulip Simon Hudon (Jul 10 2018 at 22:21):

What error do you get?

view this post on Zulip Simon Hudon (Jul 10 2018 at 22:22):

Also, can you enclose your code between three ticks:

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

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

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

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

view this post on Zulip Chris Hughes (Jul 10 2018 at 22:24):

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

view this post on Zulip Chris Hughes (Jul 10 2018 at 22:24):

If you were to put the Types after the colon.

view this post on Zulip Chris Hughes (Jul 10 2018 at 22:24):

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

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

view this post on Zulip Mario Carneiro (Jul 10 2018 at 22:40):

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

view this post on Zulip Mario Carneiro (Jul 10 2018 at 22:40):

after the definition

view this post on Zulip Ken Roe (Jul 10 2018 at 22:49):

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

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

view this post on Zulip Kenny Lau (Jul 10 2018 at 22:51):

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

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

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

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

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