def

def は、関数や項を定義するための基本的なコマンドです。

def foo := "hello"

/-- 1を足す -/
def addOne (n : Nat) : Nat := n + 1

/-- 階乗関数 -/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#guard factorial 7 = 5040

なお関数を定義するとき、隣接する同じ型の引数に対しては : を使いまわすことができます。

def add (n m : Nat) : Nat := n + m

def threeAdd (n m l : Nat) : Nat := n + m + l

where

where キーワードを使うと、定義をする前に変数を使用することができます。主に、ヘルパー関数を宣言するために使用されます。

/-- 整数 `m, n` が与えられたときに `m` 以上 `n` 以下の整数のリストを返す -/
def range (m n : Int) : List Int :=
  loop m (n - m + 1).toNat
where
  loop (start : Int) (length : Nat) : List Int :=
    match length with
    | 0 => []
    | l + 1 => loop start l ++ [start + l]

where 構文には、複数の式を同時に渡すこともできます。

/-- 自然数 `n` の素因数とその重複度のリストを返す -/
partial def primeFactorsMult (n : Nat) : List (Nat × Nat) :=
  loop 2 n [] |>.reverse
where
  /-- 自然数 `d` に対して、`n` の重複度 `μ` と `d` のペア `(d, μ)` を返す。-/
  extract (d n : Nat) : Nat × Nat :=
    if d ≤ 1 then
      (1, 0)
    else if n % d != 0 then
      (d, 0)
    else
      let (d, m) := extract d (n / d)
      (d, m + 1)

  /-- ヘルパー関数 -/
  loop (d target : Nat) (acc : List (Nat × Nat)) : List (Nat × Nat) :=
    if target ≤ 1 then
      acc
    else
      let (d, m) := extract d target
      if m = 0 then
        loop (d + 1) target acc
      else
        loop (d + 1) (target / (d ^ m)) ((d, m) :: acc)