定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。 要約 Inductiveに定義したPropのほうが使いやすいらしい Inductiveに定義したPropの各名前は、applyできる Inductive Xを定義するとX_indが自動で定…

30分プログラム、その684。昔にやった仲間はずれの判定を、もう一度やってみました。 問題はhttp://ja.doukaku.org/53/を参考に、前回の回答は仲間外れの判別 - みずぴー日記を見てください。 使い方 *Main> classify [1,1,1,1,1] Same 1 *Main> classify [1…