対話的コマンド
トップレベルコマンドのうち、# から始まるものを本書では便宜的に「対話的コマンド」と呼んでいます。これは、そうしたコマンドの多くが「式を評価した値を調べる」「式の型を調べる」など Lean から情報を得るために使用されるからです。
対話的コマンド(diagnostic command)という用語は一般的なものではありません。Lean コミュニティで通じない可能性もあります。著者は diagnostic command という用語を The Hitchhiker's Guide to Logical Verification から拝借しましたが、同じものが hash command と呼ばれているのを聞いたこともあります。決まった呼び方がないという印象です。