依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか． こういうことだろうか？ module AC-2013-5 where open import Data.Nat import Relation.Binary.PropositionalEquality …

この記事は Theorem Prover Advent Calendar 2013 1日目の記事です． 注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！ ﾊヽ／::::ヽ.ヘ===ｧ {::{/≧=＝=≦V…