## Stream: general

### Topic: Lambda syntax in Lean 4

#### 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 _


#### 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?

#### 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.

#### 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

#### Sebastian Ullrich (Apr 12 2020 at 08:47):

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

#### Mario Carneiro (Apr 12 2020 at 08:48):

where is the associativity getting declared?

#### Sebastian Ullrich (Apr 12 2020 at 08:50):

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

#### Mario Carneiro (Apr 12 2020 at 08:50):

yeah but it does that on the left too?

#### Mario Carneiro (Apr 12 2020 at 08:51):

why isn't it binder ↦ term : term

#### 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.

#### Mario Carneiro (Apr 12 2020 at 08:53):

so how does the LHS get parsed then?

#### Mario Carneiro (Apr 12 2020 at 08:53):

it's not a term after all

#### Mario Carneiro (Apr 12 2020 at 08:53):

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

#### 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.

#### Mario Carneiro (Apr 12 2020 at 08:54):

what about {{a : A}}

#### Mario Carneiro (Apr 12 2020 at 08:54):

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

#### 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

#### Mario Carneiro (Apr 12 2020 at 08:56):

what about {a : A}?

#### Mario Carneiro (Apr 12 2020 at 08:56):

that's also not valid

#### 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!

#### 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