コマンドと式¶
Lean ファイルはコマンドの列です．
import，def，theorem，inductive，structure，class，instance などはコマンドです．
一方，3，3 + 4，fun n => n + 1，Nat，P → Q などは式です．
式は Lean によって elaboration され，型が決まります． elaboration とは，ユーザが書いた構文や notation を，型情報を補いながら Lean の内部で扱う型付きの式へ変換する処理です． この処理を担当する部分を elaborator と呼びます． elaborator の詳しい仕組みは Chapter 06 で扱うので，ここでは「省略された引数や型クラス引数を補い，notation を実際の定義へ結びつける役割を持つ」と理解しておけば十分です． コマンドは式そのものではなく，名前つき定義を追加する，型を確認する，評価する，名前空間に入る，といった操作を環境に対して行います．
たとえば def コマンドは，名前つきの定義を環境に追加します．
#check は式の型を確認するためのコマンドで，#eval は計算できる式を評価するためのコマンドです．
example は，名前を残さずに小さな項や証明を型検査するための匿名の宣言です．
def typedNat : Nat := 3
def typedProposition : Prop := 2 + 2 = 4
#check typedNat
#check typedProposition
#check (fun n : Nat => n + 1)
#eval typedNat + 4
typedNat : Nat := 3 は，「typedNat という名前を定義し，その型は Nat，値は 3 である」と読みます．
同様に，typedProposition : Prop := 2 + 2 = 4 は，「typedProposition という名前をもつ命題を定義する」と読みます．
型注釈 : Nat は省略できることもありますが，講義資料では意図を明示するために書くことが多いです．
この講義資料の演習では，未完成の項や証明を表すために sorry を使うことがあります．
sorry はその場のゴールを仮に閉じるための穴で，Lean はその宣言に warning を出します．
したがって，演習中に「ここをあとで埋める」という印として使うことはできますが，完成した定義や定理には残さないものです．
sorry と tactic モードの関係は Chapter 03 で改めて扱います．