エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
Coq/Agdaのどちらを使う?
この記事はTheorem Prover Advent Calendar 14日目の記事です。 さて、登録した時点では「Agdaが多いな... この記事はTheorem Prover Advent Calendar 14日目の記事です。 さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら Σ(●△●)<Isabelleの人が一人で大半埋めてるじゃねえか!? というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。 え、CoqとAgdaのことはnotogawaさんが書いてただろって? 細けえこたぁいいんだよ! ・CoqとAgda、どちらを使うべき? 好きな方を選べば良いと思うのですが、個人的な考えを挙げます。 1:性質+証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関して