You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
7 lines
231 B
Racket
7 lines
231 B
Racket
6 years ago
|
#lang quadwriter/markdown
|
||
|
|
|
||
|
|
```
|
||
|
|
excl-middl→¬¬-elim : ∀ {A : Set} → A ⊎ ¬ A → (¬ ¬ A → A)
|
||
|
|
excl-middl→¬¬-elim (inj₁ a) = λ ¬¬a → a
|
||
|
|
excl-middl→¬¬-elim (inj₂ ¬a) = λ ¬¬a → ⊥-elim (¬¬a ¬a)
|
||
|
|
```
|