leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll