宣言的コマンド

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

Warning

宣言的コマンド(declarative command)という用語は一般的なものではなく、著者が本書で使うために考案したものです。