Dot placeholders in binders

Stream: lean4

[Eric Wieser]

A puzzle/bug report:

-- surely this should be illegal?
def foo : Nat → Nat → Nat := (fun · => ‹Nat›)

-- what does this print?
#eval foo 1 2

2

[Damiano Testa]

I am surprised that the keyboard even allows to type the definition of foo!

[Kyle Miller]

I think what's going on is that, for example, (fun · => 2) is fun x => (fun x => 2).

It's possible to use · here because the binders in fun syntax are arbitrary terms.

[Eric Wieser]

Kyle Miller said:

It's possible to use · here because the binders in fun syntax are arbitrary terms.

:double_exclamation:

[Kyle Miller]

I just saw that dot in the AlphaProof example and realized this was a sneak peak :laughing: (link to Eric's comment in that thread here)

I remember you also had a question about use · being (accidentally) legal.