News for hackers. Stuff that matters.
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Shoue on Wednesday August 07, 2019 @08:41AM (#20634130)
1) those are for pattern matching, or sum-type separators in data definitions. Also if `|` were to mean "pipe", it's actually a downgrade because the direction isn't clear. `|>` and `<|` show that they pass data to the right and left functions respectively. If it were `|` what would be the accompanying operator that passes data in the opposite direction? Unix pipe streams data, but these operators are actually function application, so I wouldn't conflate the two, the latter is a much simpler concept, `a |> f == f(a)` and `f <| a == f(a)`.

There are no comments on this comment yet.