Coq/Agdaのどちらを使う？
この記事はTheorem Prover Advent Calendar 14日目の記事です。 さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら Σ(●△●)＜Isabelleの人が一人で大半埋めてるじゃねえか！？ というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。 え、CoqとAgdaのことはnotogawaさんが書いてただろって？ 細けえこたぁいいんだよ！ ・CoqとAgda、どちらを使うべき？ 好きな方を選べば良いと思うのですが、個人的な考えを挙げます。 1:性質＋証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関して
CoqのtacticやコマンドとAgda上操作の対応 - ぼくのぬまち 出張版
この記事は Theorem Prover Advent Calendar 2013 1日目の記事です． 注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！ ﾊヽ／::::ヽ.ヘ===ｧ {::{/≧=＝=≦V:/ >:´:::::::::::::::::::::::::｀ヽ、 γ:::::::::::::::::::::::::::::::::::::::::ヽ _／/::::::::::::::::::::::::::::::::::::::::::::::ﾊ 私知ってるよ . | ll ! :::::::l::::::/|ハ::::::::∧::::i :::::::i みんなCoqの記事ばっか書くってこと ､ヾ|:::::::::|:::/｀ト-:::::/ _,X:j
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
