宣言的コマンド

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