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

Fixed link in Naturals

Browse source
This commit is contained in:
Wen Kokke 2018-06-10 21:12:26 +02:00
parent 94b3679339
commit e849d56fb3
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/plta/Naturals.lagda
View file

@ -269,7 +269,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/Equality.md %}). but will see how they are defined in Chapter [Equality](Equality).
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