宣言的コマンド

トップレベルコマンドには # から始まるものとそうでないものがあり、そうでないものを本書では便宜的に「宣言的コマンド」と呼んでいます。これは、そうしたコマンドが定義を行ったり属性を付与したりと、Lean に何かを宣言するために使われることが多いためです。

構文的には宣言的コマンドと対話的コマンドは同じ振る舞いをします。