OfNat

OfNat 型クラスは、0 や1 などの数値リテラルを特定の型の値として解釈する方法を指定します。

namespace OfNat

/-- 偶数全体 -/
inductive Even where
  | zero : Even
  | addTwo : Even → Even

-- まだ `OfNat` のインスタンスがないので、
-- `0` という数値リテラルを `Even` 型の値として解釈することはできない
#check_failure (0 : Even)

/-- `0` という数値リテラルを `Even` の項として解釈する方法を指定 -/
instance : OfNat Even 0 where
  ofNat := Even.zero

-- エラーがなくなった
#check (0 : Even)

0 や 1 などの特定の数値リテラルに対して個別に宣言するだけでなく、変数を使って一斉に OfNat のインスタンスを宣言することもできます。

/-- 有理数もどき。
約分したら等しいものは等しいというルールがないので有理数ではない -/
structure Rational where
  num : Int
  den : Nat
  inv : den ≠ 0

/-- 数値リテラル `n` を有理数として解釈する方法を指定 -/
instance (n : Nat) : OfNat Rational n where
  ofNat := { num := n, den := 1, inv := by decide }

-- 数値リテラルを `Rational` の意味で使用できる！
#check (2 : Rational)
#check (42 : Rational)

特定の数値リテラルに対してだけ OfNat を実装しないということもできます。

/-- 正の自然数全体 -/
inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

/-- 自然数 `n` を `n + 1` に相当する `Pos` の項に写す -/
def Pos.ofNatPlus (n : Nat) : Pos :=
  match n with
  | 0 => Pos.one
  | n + 1 => Pos.succ (Pos.ofNatPlus n)

/-- 数値リテラル `1, 2, 3, ...` に対して `Pos` の項と解釈する方法を指定 -/
instance (n : Nat) : OfNat Pos (n + 1) where
  ofNat := Pos.ofNatPlus n

-- エラーにならない
#check (1 : Pos)
#check (8 : Pos)
#check (42 : Pos)

-- `0` は除外したのでエラーになる
#check_failure (0 : Pos)

end OfNat