様々な引数形式

Lean tips
  • 名前付き引数〈named arguments〉と引数省略時値〈default value〉の指定
def mySub (left right :Nat) : Nat := left - right
#check mySub
#eval mySub (right := 3) (left := 5) --> 2

def mySub' (left :Nat) (right:Nat := 1) : Nat := left - right
#check mySub'
#eval mySub' (right := 3) (left := 5) --> 2
#eval mySub' (left := 5) --> 4
  • 暗黙引数： パターンマッチ／型推論で埋める引数
  • 型インスタンスパラメータ： 型クラスのインスタンス解決によって埋める引数。引数名省略可能。例： [ToString]
  • Two-dots「..」で残余明示引数〈missing explicit arguments〉。以下が例：
inductive Term where
  | var    (name : String)
  | num    (val : Nat)
  | add    (fn : Term) (arg : Term)
  | lambda (name : String) (type : Term) (body : Term)

def getBinderName : Term → Option String
  | Term.lambda (name := n) .. => some n
  | _ => none

def getBinderType : Term → Option Term
  | Term.lambda (type := t) .. => some t
  | _ => none
structure Point where
  x : Nat
  y : Nat

def Point.addX : Point → Point → Nat :=
  fun { x := a, .. } { x := b, .. } => a + b
  • 変数引数〈varible argument〉： variable宣言された変数は、その後の関数の引数として組み込まれる。セクションでスコーピングできる。
  • 構造体を引数とすると、名前付き引数としても使うことができる。ブレイス括弧が使えて、入れ子も出来る。

引数は、リストともレコード〈構造体〉とも、コンテキストデータとも受け取れる、面白い。