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

Fix broken link

Browse source
This commit is contained in:
Wen Kokke 2018-06-04 14:00:58 +01:00
parent 17e3ab38cc
commit 2f5a55c1e4
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/Naturals.lagda
View file

@ -265,7 +265,7 @@ specifies operators to support reasoning about equivalence, and adds
all the names specified in the `using` clause into the current scope. all the names specified in the `using` clause into the current scope.
In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We
will see how these are used below. We take all these as givens for now, will see how these are used below. We take all these as givens for now,
but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/Equivalence.md %}). but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/Equality.md %}).
Agda uses underbars to indicate where terms appear in infix or mixfix Agda uses underbars to indicate where terms appear in infix or mixfix
operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written