1

agda の二重否定について明確にしたいと思います。

それでも

z≡z : 0 ≡ 0
z≡z = refl

証明する方法がわかりません：

¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥
¬¬z≡z ?

のロングハンドです¬ (0 ≢ 0)。おそらく、途中で agda のイディオムを見逃してしまったのでしょう。理想的には、標準ライブラリへの参照を最小限に抑えて説明したいと思います。

4

1 に答える 1

6

で証明でき¬¬z≡zます

¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥
¬¬z≡z h = h refl
于 2013-08-30T05:03:27.110 に答える