Coqコマンドの Print/Locateを教えてもらった。 チュートリアルの一番最初にのっけておいて欲しかった。途中で挫折して読めてない後ろの方に載ってんのかもしらんが。 Check 式の型を表示。 Print 関数や型の定義を表示。 Locate Notation を展開して表示。N…

オンライン演習も終ったし、仕事がヒマな内に、Coqに戻るかと思ったけど、やはりもう色々忘れてていろいろいやになる。年とるのってやだねえ。しかし若いころは経験と理解力と忍耐力が足らんかったから余り変わってないかもしれん。 Software Foundation Bas…