パイプライン演算子

関数型言語らしく,Lean にもパイプライン演算子があります.

|> 演算子

関数 f : α → βx : α に対して x |> ff x と同じです.

def pipe₁ := [1, 2, 3, 4, 5] |> List.map (· + 10) |> List.filter (· % 2 == 0) #guard pipe₁ = [12, 14]

|>. を使用すればフィールド記法が利用できます.

def pipe₂ := [1, 2, 3, 4, 5] |>.map (· + 10) |>.filter (· % 2 == 0) #guard pipe₂ = [12, 14]

<| 演算子

関数 f : α → βx : α に対して f <| xf x と同じです.関数適用と変わらないようですが,パイプラインを使うと括弧が要らなくなるという利点があります.

#check ([[]] : List <| List Nat) #check ([[[]]] : List <| List <| List Nat)

<|$ で書くこともできます.同じ意味になりますが,<| を使うべきであるとされています.1

#check ([[]] : List $ List Nat) #check ([[[]]] : List $ List $ List Nat)
1

Lean Manual を参照.