宣言

宣言は高額商品であり、最後の定義すべきな主要の要素です。

declarationInfo ::= Name, (universe params : List Level), (type : Expr)

declar ::= 
  Axiom declarationInfo
  | Definition declarationInfo (value : Expr) ReducibilityHint
  | Theorem declarationInfo (value : Expr) 
  | Opaque declarationInfo (value : Expr) 
  | Quot declarationInfo
  | InductiveType 
      declarationInfo
      is_recursive: Bool
      num_params: Nat
      num_indices: Nat
      -- この型の名前と相互ブロック内の他の型の名前
      allIndNames: Name+
      -- **この** 型のみについてのコンストラクタの名前
      -- このブロックに含まれる可能性のある相互のコンストラクタは含まない
      constructorNames: Name*
      
  | Constructor 
      declarationInfo 
      (inductiveName : Name) 
      (numParams : Nat) 
      (numFields : Nat)

  | Recursor 
        declarationInfo 
        numParams : Nat
        numIndices : Nat
        numMotives : Nat
        numMinors : Nat
        RecRule+
        isK : Bool

RecRule ::= (constructor name : Name), (number of constructor args : Nat), (val : Expr)

宣言のチェック

すべての宣言に対して、特定の宣言に特化した追加の手続きが行われる前に、以下の予備的なチェックが行われます：

• 宣言の declarationInfo 内の宇宙パラメータは重複してはなりません。例えば、def Foo.{u, v, u} ... という宣言は禁止されています。

• 宣言の型は自由変数を持ってはなりません；「完成した」宣言の変数はすべて束縛子に対応しなければなりません。

• 宣言の型は型でなければなりません（infer declarationInfo.type の結果は Sort でなければならない）。Lean では、def Foo : Nat.succ := .. という宣言は許可されていません；Nat.succ は値であり、型ではありません。

公理

公理に対して行われる唯一のチェックは、declarationInfo が合格することを保証するすべての宣言に対して行われるチェックです。公理が有効な宇宙パラメータと有効な型を持ち、自由変数を持たない場合、その公理は環境に受け入れられます。

商

Quot についての宣言は Quot・Quot.mk・Quot.ind・Quot.lift です。これらの宣言は Lean の理論で健全であるとされる型を持ち、環境の商についての宣言はこれらの型に正確に一致しなければなりません。これらの型は許されざるほど複雑というわけではないため、カーネルの実装にハードコードされています。

定義・定理・opaque

定義・定理・opaque は型と値の両方を持つという点で興味深いものです。これらの宣言をチェックするには、宣言の値の型を推論し、その型が declarationInfo 内で定義された型と定義上等しいことを確認します。

定理の場合、declarationInfo の型はユーザが主張する型であり、したがってユーザが証明することを主張しているもので、値はユーザによってその型の証明を提供されるものです。受け取った値の型を推論することは、その証明が実際に何を証明しているかをチェックすることに等しく、定義上の等しさのチェックはその値が証明する事柄が実際にユーザが証明しようと意図したものであることを保証します。

簡約についてのヒント

簡約のヒントには、宣言がどのように展開されるべきかという情報が含まれています。abbreviation は一般的に常に展開され、opaque は展開されず、regular N は N の値によって展開されるかどうかが決定します。regular の簡約のヒントは定義の「高さ」に対応しています。この用語はその定義自体の定義に用いられている宣言の数を指します。定義 y を参照する値を持つ定義 x の高さは　y より大きくなります。