patch for strict markdown
parent
cceec34df9
commit
28b58f8c62
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -1,7 +1,5 @@
|
||||
#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)
|
||||
foo
|
||||
```
|
Loading…
Reference in New Issue