Lambda syntax in Lean 4

Stream: general

[Uranus Testing]

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]

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]

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]

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]

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

[Mario Carneiro]

where is the associativity getting declared?

[Sebastian Ullrich]

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

[Mario Carneiro]

yeah but it does that on the left too?

[Mario Carneiro]

why isn't it binder ↦ term : term

[Sebastian Ullrich]

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]

so how does the LHS get parsed then?

[Mario Carneiro]

it's not a term after all

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

what about {{a : A}}

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

what about {a : A}?

[Mario Carneiro]

that's also not valid

[Patrick Massot]

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]

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.