Lean Prover コマンド紹介

Lean4 には # をつけて呼び出せるコマンドがいくつかあります．ほかの言語ではあまり見ない機能ですが，慣れれば大変便利ですので，ぜひ使い方を覚えていただきたいと思います．ここでは使用頻度が高いと思われるものに限ってご紹介しますが，全コマンドのリストが #help command で確認できますので，興味のある方はそちらも試してみてください．

#eval, #check, #guard_msgs, #guard, #print, #find の6コマンドを紹介します．

今回のコードも Lean web editor で実際に試すことができます．コピーして試してみてください．