名前付き引数

Lean では，関数に引数を渡すときに順序ではなく名前で引数を指定することができます．

/-- 足したり掛けたりする関数 -/
def addMul (n m : Nat) := n + m * m

-- 通常, 引数は順序で指定されるが
#guard addMul 2 3 = 11

-- 名前付き引数を使うと，引数の順序を変えることができる
#guard addMul (m := 3) (n := 2) = 11