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.
typesetting/quad/qtest/test-symbol.rkt

8 lines
232 B
Racket

#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)
```