■

Coqコマンドの Print/Locateを教えてもらった。
チュートリアルの一番最初にのっけておいて欲しかった。途中で挫折して読めてない後ろの方に載ってんのかもしらんが。

• Check

式の型を表示。

• Print

関数や型の定義を表示。

• Locate

Notation を展開して表示。

Notationは scopeを変えることで多重定義みたいなことが出来るので、Locateでずらずら出て来て焦る。