Zulip Chat Archive
Stream: new members
Topic: Operator sections
Bhavik Mehta (Nov 13 2019 at 13:48):
Does lean have any equivalent of Haskell's operator sections?
Edward Ayers (Nov 13 2019 at 15:50):
You can do
#check (× nat) int -- int × nat #check (+ 3) 2 #check ((×) nat) int -- nat × int #check ((+) 3) 2
But (3 +) is a parse error.
Bhavik Mehta (Nov 13 2019 at 15:57):
Ah so I can do sections only on one side - thanks!
Last updated: Dec 20 2023 at 11:08 UTC