1

I want some clarification on double negations in agda.

even though 

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

I cannot figure out how to prove:

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

Which is long hand for ¬ (0 ≢ 0). Perhaps I've missed an agda idiom somewhere along the way. Idealy I'd like an explanation with minimal reference the standard library.

4

1 回答 1

6

你可以¬¬z≡z证明

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