対話的コマンド

トップレベルコマンドのうち、# から始まるものを本書では便宜的に「対話的コマンド」と呼んでいます。これは、そうしたコマンドの多くが「式を評価した値を調べる」「式の型を調べる」など Lean から情報を得るために使用されるからです。

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