Agda

ブラウザ上でAgdaを試せるサイトを作ってみた

この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です.Agdaがコンパイルできないんだがとか,agda-modeってEmacsだけなんでしょ?とか,そういった話をちょくちょく耳にするし,ProofSummit2014で明日の記事担当のamutakeくんがブラウザからC…

「依存関係のある値のうちの一部を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…

anarchy proofのAgda版作った

全国一億三千万のAgdarの皆様に送る Agda Challenge最近chaton haskellがchaton agdaと化していたりすることもあり,anarchy proofがうらやましくてAgda版が欲しい人いっぱいいるのではないかと思って作ってみた.開発中にステージング環境を作り近くの数人…

Agdaとフォントと微妙な設定

Agda書くとみんなフォントに困る…と,思う.Agda標準ライブラリの時点で_⊔_とか_⊎_とか⟨_⟩とか普通のランゲッジでは使わないような文字入りの演算が目白押しだ.当然下手なフォント設定すると正しく表示されない.プログラミングに適したmonospaceのフォント…

Agdaはじめました

あぐださん!あぐださんヤッホ! Agda2に手を出してみた.とりあえずインストールし文法とかagda-modeとかをザックリとだが覚え,クイックソートを止められるあたりまで把握したので,練習としてData.Natに無さげだった速い冪乗を書いてみることに.とりあえ…