Connectives: changes a punctuation before a code block
This commit is contained in:
parent
9902053680
commit
a08d25d6a9
1 changed files with 1 additions and 1 deletions
|
@ -450,7 +450,7 @@ paradoxical situation. Given evidence that `⊥` holds, we might
|
|||
conclude anything! This is a basic principle of logic, known in
|
||||
medieval times by the Latin phrase _ex falso_, and known to children
|
||||
through phrases such as "if pigs had wings, then I'd be the Queen of
|
||||
Sheba". We formalise it as follows.
|
||||
Sheba". We formalise it as follows:
|
||||
\begin{code}
|
||||
⊥-elim : ∀ {A : Set}
|
||||
→ ⊥
|
||||
|
|
Loading…
Reference in a new issue