Skip to content

Commit c462e43

Browse files
doc: improve docstrings for pipe operators (#13864)
This PR updates the pipe operator docstrings for accurracy and helpfulness. Such operators are not idiomatic Haskell, so the old text was incorrect, and it's better to explain the behavior than to reference other languages anyway.
1 parent bf38e59 commit c462e43

1 file changed

Lines changed: 7 additions & 5 deletions

File tree

src/Init/Notation.lean

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -514,9 +514,10 @@ macro_rules
514514
| `(bif $c then $t else $e) => `(cond $c $t $e)
515515

516516
/--
517-
Haskell-like pipe operator `<|`. `f <| x` means the same as `f x`,
518-
except that it parses `x` with lower precedence, which means that `f <| g <| x`
519-
is interpreted as `f (g x)` rather than `(f g) x`.
517+
A pipe operator that feeds values from the right into functions on the left.
518+
519+
`f <| x` means the same as `f x`, except that it parses `x` with lower precedence, which means that
520+
`f <| g <| x` is interpreted as `f (g x)` rather than `(f g) x`.
520521
-/
521522
syntax:min term " <| " term:min : term
522523

@@ -538,8 +539,9 @@ macro_rules
538539
`($f $a)
539540

540541
/--
541-
Haskell-like pipe operator `|>`. `x |> f` means the same as `f x`,
542-
and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
542+
A pipe operator that feeds values from the left into functions on the right.
543+
544+
`x |> f` means the same as `f x`, and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
543545
-/
544546
syntax:min term " |> " term:min1 : term
545547

0 commit comments

Comments
 (0)