Lean doc suggestion

Stream: lean4

[Tom]

I'd like to make a small mod to section http://lovettsoftware.com/lean4/functions.html#pipelining.

The section says "The forward pipeline |> operator takes a function and an argument and return a value. In contrast, the backward pipeline <| operator takes an argument and a function and returns a value."

However, the wording seems a bit "backwards" to me: Ok to replace post a PR and replace it with e.g.

"The forward pipeline |> operator a |> f takes an argument a and a function f and returns f a. The backward pipeline <| operator reverses the order of f and a: For example, f <| a again returns f a ."

[Tom]

(Also, my macro-fu still needs work but just looking at the definitions of operator |> and <|, it seems the parser is just a standard precedence climbing/pratt parser; in which case, would it make sense to also mention that the former is left associative and the latter is right-associative?)

[Mario Carneiro]

Yes, |> is left-associative and <| is right-associative. The docstring on each should say as much, and you can test it like this:

#check fun a (b:_→_) (c:_→_→_) => a |> b |> c -- c (b a)
#check fun a (b:_→_) (c:_→_→_) => (a |> b) |> c -- c (b a)
#check fun a (b:_→_) (c:_→_→_) => a |> (b |> c) -- c b a

#check fun (a:_→_→_) (b:_→_) c => a <| b <| c -- a (b c)
#check fun (a:_→_→_) (b:_→_) c => (a <| b) <| c -- a b c
#check fun (a:_→_→_) (b:_→_) c => a <| (b <| c) -- a (b c)

[Mario Carneiro]

I'm not even sure I want to use the terms "forward pipeline" and "backward pipeline" here, I don't think it's obvious which way is forward. It's also worth mentioning that <| is used 40 times more often than |>

[Mario Carneiro]

amusingly, <| and $ are about equally used in lean 4, although I believe the latter is deprecated

[Chris Lovett]

Note the official docs live here: https://leanprover.github.io/lean4/doc/functions.html?highlight=operator%20takes%20a%20function#pipelining my site was just a temporary staging location until the monads PR was merged (which it is now).

[Chris Lovett]

I took a crack at fixing the documentation here: https://github.com/leanprover/lean4/pull/1594

[Tom]

Thanks! As a newcomer, I felt reluctant to make documentation changes without someone else "ok"-ing them, hence why I've not gone ahead and done this. I appreciate you helping out! I made some minor wording suggestions on the PR. Thanks a lot!