variable

variable は、定理や関数の引数を宣言するためのコマンドです。

たとえば以下の関数と命題に対して、引数の α : Type と l : List α は共通です。

/-- 連結リストの最後の要素を取り出す -/
def last? {α : Type} (l : List α) : Option α :=
  match l with
  | [] => none
  | [a] => some a
  | _ :: xs => last? xs

theorem nng_list_length {α : Type} (l : List α) : l.length >= 0 := by simp

variable コマンドを利用すると、共通の引数を宣言してまとめておくことができます。

variable {α : Type} (l : List α)

/-- 連結リストの最後の要素を取り出す -/
def last? (l : List α) : Option α :=
  match l with
  | [] => none
  | [a] => some a
  | _ :: xs =>last? xs

theorem nng_list_length : l.length >= 0 := by simp

上記の２つの例で引数の l : List α を省略できるかどうかに違いがありますが、これは返り値の型に現れているかどうかに依ります。