Lean 4 receiver syntax #33

New issue

Open

opened 2026-07-01 10:48:23 +02:00 by st · 0 comments

st commented 2026-07-01 10:48:23 +02:00

Owner

Copy link

x.f(y) desugar to f(x, y)

What's more principled? Allowing it in general or tying it to the type of x defining the method specififally?

`x.f(y)` desugar to `f(x, y)` What's more principled? Allowing it in general or tying it to the type of `x` defining the method specififally?

st added the

rfc

label 2026-07-01 10:48:23 +02:00

Sign in to join this conversation.

No Branch/Tag specified

Branches Tags

main

No results found.

Labels

Clear labels   

bug

  

hack

  

planned

  

rfc

  

surprise

No labels

bug

hack

planned

rfc

surprise

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

st/amelie#33

No description provided.