パイプライン演算子

Lean には前方パイプライン演算子 |> と後方パイプライン演算子 <| が用意されています。これは、関数適用を括弧で囲むことなく、自然な順序で記述できるようにするためのものです。

前方パイプライン演算子

前方パイプライン演算子 |> は、a |> f と書くことで f a と同じ意味になります。

variable {α β : Type}

example (a : α) (f : α → β) : (a |> f) = f a := by rfl

これがなぜ嬉しいかというと、データに関数を次々と適用して処理していくような処理を括弧なしで、自然な順序で書くことができるからです。

/- info: 20 -/
#eval [1, 2, 3, 4, 5]
  |> List.filter (· % 2 = 0)
  |> List.map (· ^ 2)
  |> List.sum

後方パイプライン演算子

後方パイプライン演算子 <| は、f <| a と書くことで f a と同じ意味になります。

variable {α β : Type}

example (a : α) (f : α → β) : (f <| a) = f a := by rfl