Skip to content

chore: improve docstring of pipe operators #10413

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore: improve docstring of pipe operators #10413

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/Init/Notation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -551,6 +551,8 @@ macro_rules
/--
Haskell-like pipe operator `|>`. `x |> f` means the same as `f x`,
and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
Comment on lines 552 to 553
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a strict improvement as-is.

However, while you're at it, perhaps something like this this would be good too?

Suggested change
Haskell-like pipe operator `|>`. `x |> f` means the same as `f x`,
and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
The pipe operator `|>`, which allows a function to be placed _after_ its argument.
`x |> f` is equivalent to `f x`, and it chains such that `x |> f |> g` is interpreted as `g (f x)`. This
directs readers' attention to an initial value and a sequence of transformations, instead of
centering the function.

This operator is not widely used in Haskell, where & is more common for this purpose. It's certainly very common in F#, and I believe it's also popular in many Haskell-derived languages. I think it's also useful to point out why someone might want to write the argument before the function.


Compare to `x |>.f`, without a space, a shorthand for (x).f`.
-/
syntax:min term " |> " term:min1 : term

Expand Down
2 changes: 2 additions & 0 deletions src/Lean/Parser/Term.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1049,6 +1049,8 @@ If present, the identifier `h` is bound to a proof of `x = e`. -/
/--
`e |>.x` is a shorthand for `(e).x`.
It is especially useful for avoiding parentheses with repeated applications.

Compare to `e |> .x`, with a space, a shorthand for .x (e)`.
-/
@[builtin_term_parser] def pipeProj := trailing_parser:minPrec
" |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
Expand Down
Loading