CoqのtacticやコマンドとAgda上操作の対応 - ぼくのぬまち 出張版この記事は Theorem Prover Advent Calendar 2013 1日目の記事です． 注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！ ﾊヽ／::::ヽ.ヘ===ｧ {::{/≧=＝=≦V:/ >:´:::::::::::::::::::::::::｀ヽ、 γ:::::::::::::::::::::::::::::::::::::::::ヽ _／/::::::::::::::::::::::::::::::::::::::::::::::ﾊ 私知ってるよ . | ll ! :::::::l::::::/|ハ::::::::∧::::i :::::::i みんなCoqの記事ばっか書くってこと ､ヾ|:::::::::|:::/｀ト-:::::/ _,X:j
