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

fixed typo

Browse source
This commit is contained in:
Michel Steuwer 2018-05-13 16:37:16 +01:00 committed by GitHub
parent a664d66bd5
commit aefc56cd03
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Naturals.lagda
View file

@ -259,8 +259,7 @@ opens that module, that is, adds all the names specified in the
`using` clause into the current scope. In this case the names added `using` clause into the current scope. In this case the names added
are `_≡_`, the equivalence operator, and `refl`, the name for evidence are `_≡_`, the equivalence operator, and `refl`, the name for evidence
that two terms are equal. The third line takes a record that that two terms are equal. The third line takes a record that
specifies operators to support reasoning about equivalence, specifies operators to support reasoning about equivalence, and adds
dds
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,