2007-10-01から1ヶ月間の記事一覧
Coqで証明をする動画を作って、にこにこ動画に公開した。 http://www.nicovideo.jp/watch/sm1276083
次に、このPeanoPositiveを使って、PeanoZという整数型を作った。
まずこの前のコードに引き算のレンマを加えて、PeanoPositive.vとしてまとめた。
この前作ったマイポジティブ型は、ペアノの公理を元にした形式化だったので、それを使って、ペアノゼットという整数型を作ってみた。 既存のポジティブ型とマイポジティブ型との間の同型対応は、前回示してあるので、それをもとにしている既存のZ型とペアノ…