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

fixing ndash and mdash

Browse source
This commit is contained in:
wadler 2018-01-01 19:03:51 -02:00
parent bf6c5a0602
commit 33640cf86e
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Naturals.lagda
View file

@ -204,7 +204,7 @@ A philosopher might note that our reference to the first day, second
day, and so on, implicitly involves an understanding of natural day, and so on, implicitly involves an understanding of natural
numbers. In this sense, our definition might indeed be regarded as in numbers. In this sense, our definition might indeed be regarded as in
some sense circular. We won't worry about the philosophy, but are ok some sense circular. We won't worry about the philosophy, but are ok
with taking some intuitive notions--such as counting--as given. with taking some intuitive notions---such as counting---as given.
While the natural numbers have been understood for as long as people While the natural numbers have been understood for as long as people
could count, the inductive definition of the natural numbers is relatively could count, the inductive definition of the natural numbers is relatively
@ -217,7 +217,7 @@ presented by a new method), published the following year.
## A useful pragma ## A useful pragma
In Agda, any line beginning `--`, or any code enclosed between `{-` In Agda, any text following `--` or enclosed between `{-`
and `-}` is considered a *comment*. Comments have no effect on the and `-}` is considered a *comment*. Comments have no effect on the
code, with the exception of one special kind of comment, called a code, with the exception of one special kind of comment, called a
*pragma*, which is enclosed between `{-#` and `#-}`. *pragma*, which is enclosed between `{-#` and `#-}`.

2
src/Properties.lagda
View file

@ -78,7 +78,7 @@ data ℕ : Set where
zero : ℕ zero : ℕ
suc : ℕ → ℕ suc : ℕ → ℕ
\end{code} \end{code}
This tells us that `zero` is a natural--the *base case*--and that if This tells us that `zero` is a natural---the *base case*---and that if
`m` is a natural then `suc m` is also a natural---the *inductive `m` is a natural then `suc m` is also a natural---the *inductive
case*. case*.