Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
agda の二重否定について明確にしたいと思います。
それでも
z≡z : 0 ≡ 0 z≡z = refl
証明する方法がわかりません:
¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥ ¬¬z≡z ?
のロングハンドです¬ (0 ≢ 0)。おそらく、途中で agda のイディオムを見逃してしまったのでしょう。理想的には、標準ライブラリへの参照を最小限に抑えて説明したいと思います。
¬ (0 ≢ 0)
で証明でき¬¬z≡zます
¬¬z≡z
¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥ ¬¬z≡z h = h refl