2014-09-20から1日間の記事一覧

An exercise in dependent types (解答編)

http://lkozima.hatenablog.com/entry/2014/09/15/013735 の続き。ホーア論理の健全性の証明をやろうとしていたのでした。一箇所ちょっと難しいところがあるような気がしたのでそれについて書こうとしていたのですが,あれこれ調べているうちに簡単な解決策…