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

Merge pull request #501 from ChefYeum/patch-1

Browse source 
Add documentation link to Agda pragmas
This commit is contained in:
Philip Wadler 2020-08-05 08:36:01 +01:00 committed by GitHub
commit b372721501
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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/part1/Naturals.lagda.md
View file

@ -941,7 +941,7 @@ Such a pragma can only be invoked once, as invoking it twice would
raise confusion as to whether `2` is a value of type `ℕ` or type raise confusion as to whether `2` is a value of type `ℕ` or type
`Data.Nat.ℕ`. Similar confusions arise if other pragmas are invoked `Data.Nat.ℕ`. Similar confusions arise if other pragmas are invoked
twice. For this reason, we will usually avoid pragmas in future chapters. twice. For this reason, we will usually avoid pragmas in future chapters.
Information on pragmas can be found in the Agda documentation. Information on pragmas can be found in the (Agda documentation)[https://agda.readthedocs.io/en/v2.6.1/language/pragmas.html].
## Unicode ## Unicode