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

fixed bug in Connectives

Browse source
This commit is contained in:
wadler 2018-03-14 18:34:46 -03:00
parent 771bd2de5d
commit b31d8eba50
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Connectives.lagda
View file

@ -469,7 +469,7 @@ The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim`
is equal to any arbitrary function from `⊥`. is equal to any arbitrary function from `⊥`.
\begin{code} \begin{code}
uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ () uniq-⊥ h ()
\end{code} \end{code}
The pattern matching on the left-hand side is essential. Using The pattern matching on the left-hand side is essential. Using
the absurd pattern asserts there are no possible values for `w`, the absurd pattern asserts there are no possible values for `w`,