その他の便利な機能

インスタンスのためのコンストラクタ記法

裏側では、型クラスは構造体型であり、インスタンスはこれらの型の値です。唯一の違いは、Leanが型クラスに関する追加情報（どのパラメータが出力パラメータであるかなど）を保存していることと、インスタンスが検索のために登録されていることです。構造体型の値は通常 ⟨...⟩ 構文か波括弧とフィールドを使って定義されます。インスタンスは通常 where を使って定義されます。これらの構文は両方の定義どちらでも使うことができます。

例えば、林業に対するアプリケーションでは樹木を次のように表現します：

structure Tree : Type where
  latinName : String
  commonNames : List String

def oak : Tree :=
  ⟨"Quercus robur", ["common oak", "European oak"]⟩

def birch : Tree :=
  { latinName := "Betula pendula",
    commonNames := ["silver birch", "warty birch"]
  }

def sloe : Tree where
  latinName := "Prunus spinosa"
  commonNames := ["sloe", "blackthorn"]

これら3つの記法は等価です。

同じように、型クラスのインスタンスもこれら3つすべての記法で定義可能です：

class Display (α : Type) where
  displayName : α → String

instance : Display Tree :=
  ⟨Tree.latinName⟩

instance : Display Tree :=
  { displayName := Tree.latinName }

instance : Display Tree where
  displayName t := t.latinName

一般的に、インスタンスには where 構文を使用し、構造体には波括弧構文を使用します。⟨...⟩ の構文は、構造体型がタプルとよく似ていることを強調する際には便利です。つまり、フィールドに名前がついてはいますが、そのことがあまり重要でない場合です。しかし、ほかの選択肢を使うことが理にかなっている状況もあります。特に、ライブラリがインスタンス値を構築する関数を提供する場合です。このような関数の使い方として最も簡単な方法は、インスタンス宣言の := の後にこの関数を呼び出すのことです。

例の記述

Leanのコードを試したい場合、#eval や #check コマンドよりも定義を使った方が便利な場合があります。第一に、定義は出力を生成しないので、読者の注意を最も興味深い出力に集中させることができます。第二に、Leanのプログラムを書くにあたって型シグネチャから始めることが最も簡単で、これによってプログラムを書いている間により良いエラーメッセージと支援をLeanから得ることができます。一方、#eval と #check はLeanが与えられた式から型を決定できるコンテキストで使用することが最も簡単です。第三に、#eval は関数のように、ToString や Repr インスタンスを持たない式には使用できません。最後に、複数行にわたる do ブロック、let 式、その他の構文形は #eval や #check で型注釈を記述することが特に難しいです。　というのもシンプルにそれらに求められる括弧がどう挿入されるかの予測が難しいからです。

これらの問題を回避するために、Leanはソースファイル内の例を明示的に示すことをサポートしています。例とは名前のない定義のようなものです。例えば、コペンハーゲンの緑地でよくみられる鳥についての空でないリストは以下のように書くことができます。

example : NonEmptyList String :=
  { head := "Sparrow",
    tail := ["Duck", "Swan", "Magpie", "Eurasian coot", "Crow"]
  }

例は引数を受け付けることで関数を定義することもできるでしょう：

example (n : Nat) (k : Nat) : Bool :=
  n + k == k + n

これは裏側で関数を作成しますが、この関数には名前がなく、呼び出すことができません。とはいえ、この関数は任意の型や未知の型の値でライブラリがどのように使えるのかを示すのに便利です。ソースファイルでは、example 宣言はその例がライブラリの概念をどのように表現しているかを説明するコメントと組み合わせるのが最適です。