From f939eebf5b7f83c61acfd50f63197c75c03e4913 Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 14 Feb 2018 21:10:07 -0200 Subject: [PATCH] fixed bug in LogicAns --- src/LogicAns.lagda | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/LogicAns.lagda b/src/LogicAns.lagda index a166bd58..30decfc8 100644 --- a/src/LogicAns.lagda +++ b/src/LogicAns.lagda @@ -27,13 +27,6 @@ ex3 em k with em ... | inj₁ a = a ... | inj₂ ¬a = k (λ a → ⊥-elim (¬a a)) -ex4 : de-morgan′ → ¬¬-elim -ex4 dem ¬¬a = fst (dem (obvs ¬¬a)) - where - obvs : ∀ {A : Set} → ¬ ¬ A → ¬ (¬ A ⊎ ¬ ⊤) - obvs ¬¬a (inj₁ ¬a) = ¬¬a ¬a - obvs ¬¬a (inj₂ ¬⊤) = ¬⊤ tt - help′ : excluded-middle → ∀ {A B : Set} → ¬ (A × B) → ¬ A ⊎ ¬ B help′ em ¬a×b with em | em ... | inj₁ a | inj₁ b = ⊥-elim (¬a×b (a , b))