コマンド

Lean は定理証明支援系であると同時に汎用プログラミング言語です．他の多くのプログラミング言語と同様，繰り返しや条件分岐を表現できますし，新しい型を定義したり，新しい関数を定義したりすることもできます．こういったことは他のプログラミング言語を知っている人にとっては，既になじみ深いものでしょう．

一方で Lean は純粋関数型言語であるとともに，帰納型を伴う Calculus of Construction と呼ばれる型システムに基づくという，あまり一般的でない特徴を持っています．また，Lean は文法が完全に拡張可能という特徴もあります．パーサ・エラボレータ・タクティク・プリティプリンタなどをユーザが自由に変更・拡張することができるのです．

このセクションでは，Lean のコマンドについてコード例を元に説明します．