2014-07-28から1日間の記事一覧
MoreInd.v 帰納法のための明示的な証明オブジェクト を読む。目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。そういうわけで、以前の l=rev l -> pal l も、 list Xのコンストラクタを変えて、新たな帰納法の原…
MoreInd.v 帰納法のための明示的な証明オブジェクト を読む。目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。そういうわけで、以前の l=rev l -> pal l も、 list Xのコンストラクタを変えて、新たな帰納法の原…