zyxwv https://blog.hatena.ne.jp/zyxwv/ zyxwvの日記 https://zyxwv.hatenadiary.org/ Agda Agda2 まじわかんない。心折れそう。とりあえず agda-mode で使い方がわかったやつを適当 メモ。そのうち追加します。 C-c C-x C-l agda で証明を開始。 ? 証明がよくわからないところは ? で埋める。 assoc x y z = ? これで C-c C-x C-l とすると ? がゴール(用法が正しいか不明)になる。 C-c C-c 場合分けを自動でやってくれる。 assoc x y z = {! !} が assoc zero y z = {! !} assoc (suc y) y' z = {! !} になる。 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fzyxwv.hatenadiary.org%2Fentry%2F20080711%2F1215746927" title=" Emacs agda-mode の使い方 - zyxwvの日記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2008-07-11 12:28:47 rich https://zyxwv.hatenadiary.org/entry/20080711/1215746927 1.0 100%