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

Equality chapter: removes a redundant verb

Browse source
This commit is contained in:
Marko Dimjašević 2019-01-12 14:29:39 +01:00 • committed by Wen Kokke
parent 1941aab79d
commit 434b8f5be5
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/plfa/Equality.lagda
View file

@ -399,7 +399,7 @@ even-comm : ∀ (m n : ℕ)
even-comm m n ev rewrite +-comm n m = ev even-comm m n ev rewrite +-comm n m = ev
\end{code} \end{code}
Here `ev` ranges over evidence that `even (m + n)` holds, and we show Here `ev` ranges over evidence that `even (m + n)` holds, and we show
that it is also provides evidence that `even (n + m)` holds. In that it also provides evidence that `even (n + m)` holds. In
general, the keyword `rewrite` is followed by evidence of an general, the keyword `rewrite` is followed by evidence of an
equality, and that equality is used to rewrite the type of the equality, and that equality is used to rewrite the type of the
goal and of any variable in scope. goal and of any variable in scope.