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

Connectives: fixes an explanation of simplification

Browse source
This commit is contained in:
Marko Dimjašević 2019-01-30 16:24:30 +01:00 • committed by Wen Kokke
parent 189afeed9c
commit 9902053680
1 changed files with 2 additions and 2 deletions

4
src/plfa/Connectives.lagda
View file

@ -378,8 +378,8 @@ uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl
\end{code}
The pattern matching on the left-hand side is essential. Replacing
`w` by `inj₁ x` allows both sides of the equation to simplify to the
same term, and similarly for `inj₂ y`.
`w` by `inj₁ x` allows both sides of the propositional equality to
simplify to the same term, and similarly for `inj₂ y`.
We set the precedence of disjunction so that it binds less tightly
than any other declared operator: