7.2. インスタンスの宣言（Instance Declarations）🔗

以下の NatTree の定義に対して：

以下の BEq インスタンスは失敗します：

これは左右両方の再帰呼び出しでエラーが発生しています：

failed to synthesize
  BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.

NatTree.beq のような適切な再帰関数を与え：

次のステップでインスタンスを作成できます：

もしくは同等ですが、匿名コンストラクタ構文を使うことでも作成できます：

この NatRoseTree の定義では、定義されている型は別の帰納型コンストラクタ（ Array ）の下に入れ子になっています：

バラの木の等価性をチェックするには、配列の等価性をチェックする必要があります。しかし、インスタンスは通常それ自身の定義中にインスタンス統合のために利用できないため、たとえ NatRoseTree.beq が再帰関数であり、それ自身の定義のスコープ内にあるにもかかわらず以下の定義は失敗します。

failed to synthesize
  BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

これを解決するために、let 束縛されたローカルの BEq NatRoseTree インスタンスを作成します：

インスタンス統合時に、子に対して配列の等価性を使用することで let 束縛されたインスタンスが発見されて使用されます。

DecidableEq α は (a b : α) → Decidable (Eq a b) の省略形であるため、この例のように直接引数を使うことができます：

型 StringList はモノ射な文字列リストを表します：

以下の DecidableEq インスタンスを定義しようとすると、内部の termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if をエラボレートする際にインスタンス統合が呼び出されますが、インスタンスがそれ自身の定義でインスタンス統合に利用できないため失敗します：

failed to synthesize
  Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

しかし、これは通常の Lean の関数であるため、明示的に与えられた名前を再帰的に参照することができます：

OfNat Nat のデフォルトインスタンスは、他の型情報がない場合に自然数リテラルに対して Nat を選択するために使用されます。これは Lean の標準ライブラリで優先度 100 で宣言されています。この偶数の表現では、偶数はその半分の値で表現されています：

以下のインスタンスでは、数値リテラルを小さな Even に使用することができます（型クラスインスタンス検索の深さの制限により、任意の大きさのリテラルに使用することはできません）：

{ half := 0 }

{ half := 17 }

{ half := 127 }

これらを優先度が 100 以上のデフォルトインスタンスとして指定すると、 Nat の代わりに使用されます：

{ half := 0 }

{ half := 17 }

偶数でない数字では依然として OfNat Nat インスタンスが使用されます：

5