読者です 読者をやめる 読者になる 読者になる

Coq

「依存関係のある値のうちの一部をrewriteしようとしたときの問題」をAgdaで書くとどうなるか

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

CoqのtacticやコマンドとAgda上操作の対応

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