michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixed bug in LogicAns

Browse source
This commit is contained in:
wadler 2018-02-14 21:10:07 -02:00
parent 9114aad7b3
commit f939eebf5b
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/LogicAns.lagda
View file

@ -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))