keyword/named/labelled parameters

Stream: Is there code for X?

[Jianlin Li]

Hi everyone :blush:
In Lean, all function parameters are positional rather than labelled. I can imagine faking named parameters by having the function take a struct as input, so arguments can be provided out of order.
But I’m wondering — is there already a library (or maybe a plugin) that supports true named parameters in Lean, along with partial application (currying/uncurrying)? Or any tips on how one might implement such a thing? :folded_hands:

[Aaron Liu]

You can already do named parameters in Lean with the (name := value) syntax

[Kyle Miller]

It supports partial application too :-)

[Kyle Miller]

e.g.

variable (lst : List Bool)

#check List.map (l := lst)
/-
fun f => List.map f lst : (Bool → ?m.10) → List ?m.10
-/

[Aaron Liu]

#check List.mergeSort [1, 2, 3]
#check List.mergeSort [1, 2, 3] fun a b => Nat.xor a b < a
#check List.mergeSort (le := fun a b => Nat.xor a b < a) [1, 2, 3]
#check List.mergeSort (le := fun a b => Nat.xor a b < a)