diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 3c524d5327d9..f034f0172156 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -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)`. + +Compare to `x |>.f`, without a space, a shorthand for (x).f`. -/ syntax:min term " |> " term:min1 : term diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 30736df07b0c..ce925f4e6e62 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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