Zulip Chat Archive

Stream: general

Topic: Lambda syntax in Lean 4


view this post on Zulip Uranus Testing (Apr 11 2020 at 10:31):

Wow! Can it break anything?

new_frontend

syntax "(" term "↦" term ")" : term
macro_rules `(($x  $y)) => `(fun $x => $y)

#check (x  x + 1)
#check λ (x : Nat) => x + 1

example : (x  x + 1) 5 = 6 :=
Eq.refl 6

example : (x  x + 1) = (λ x => x + 1) :=
Eq.refl _

view this post on Zulip Sebastian Ullrich (Apr 11 2020 at 20:57):

Hah nice, someone is actually playing with that. You can drop the parens if you set a precedence on the arrow:

new_frontend

syntax term "↦":1024 term : term
macro_rules `($x  $y) => `(fun $x => $y)

#check x  x + 1
#check (x : Nat)  x + 1

example : (x  x + 1) 5 = 6 :=
Eq.refl 6

example : (x  x + 1) = (λ x => x + 1) :=
Eq.refl _

or, of course, just

notation x "↦":1024 y => fun x => y

Next task: finding and implementing a sensible syntax for multiple parameters?

view this post on Zulip Sebastian Ullrich (Apr 11 2020 at 21:00):

Breaking anything by introducing new syntax should be hard as long as it doesn't cover existing syntax, and the leading token isn't already used somewhere else as a non-leading token, like in the [a,b[ example.

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:14):

Well, if they are in the same binder group then you could use the syntax (a b : Nat) ↦ a, and if they are not then you could just right associate as in (a : Nat) ↦ (b : Nat) ↦ a

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 08:47):

Yeah, looks fine and should even work out of the box with the above definition

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:48):

where is the associativity getting declared?

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 08:50):

term is short for term:0, so it will eat any following binders and "↦":1024

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:50):

yeah but it does that on the left too?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:51):

why isn't it binder ↦ term : term

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 08:52):

There is no real LHS. If you start a term syntax with term, the syntax macro recognizes the left recursion and refactors it into a trailing parser. The real parser is "↦":1024 term, it is triggered on the arrow.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:53):

so how does the LHS get parsed then?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:53):

it's not a term after all

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:53):

unless you need it to conform to the term grammar anyway?

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 08:53):

Since binders may contain arbitrary patterns, they are in fact parsed as terms. (a : A) (b : B) is an application of type annotations.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:54):

what about {{a : A}}

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:54):

that's not a valid term in lean 3 at least

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 08:56):

Uh, I don't think we have strict implicits atm... not sure if there was a concious decision to remove them

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:56):

what about {a : A}?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:56):

that's also not valid

view this post on Zulip Patrick Massot (Apr 12 2020 at 09:07):

Sebastian Ullrich said:

Uh, I don't think we have strict implicits atm... not sure if there was a concious decision to remove them

But those are crucial!

view this post on Zulip Sebastian Ullrich (Apr 12 2020 at 09:32):

Ah, my description was overly simplified. terms are valid binders, but the other annotations are there as well. So the syntax above is not quite complete yet.


Last updated: May 14 2021 at 00:42 UTC