■

Sparkleで証明できるにもかかわらず、Cleanでは正しくない命題の例。

forall n::Int.(n > 0)=>(n+1 > 0)

何故ならCleanでIntは32ビット整数だから。