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)`.
[ Parent
| on HN ]
There are no comments on this comment yet.