From 33640cf86ea867367dec89472eae1f3c05dcf884 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 1 Jan 2018 19:03:51 -0200 Subject: [PATCH] fixing ndash and mdash --- src/Naturals.lagda | 4 ++-- src/Properties.lagda | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 85bd51df..321343e7 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -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 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 -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 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 -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 code, with the exception of one special kind of comment, called a *pragma*, which is enclosed between `{-#` and `#-}`. diff --git a/src/Properties.lagda b/src/Properties.lagda index 72ac262f..6163c19b 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -78,7 +78,7 @@ data ℕ : Set where zero : ℕ suc : ℕ → ℕ \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 case*.