From 84556ab62e56068a0c7940f056a90021afac8d96 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Sat, 8 Feb 2020 14:30:29 +0000 Subject: [PATCH] Minor fix --- src/plfa/part1/Naturals.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 3c7d9e75..09961da0 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -242,7 +242,7 @@ is permitted to type `0` as shorthand for `zero`, `1` as shorthand for `suc zero`, `2` as shorthand for `suc (suc zero)`, and so on. The pragma must be given a previously declared type (in this case `ℕ`) with precisely two constructors, one with no arguments (in this case `zero`), -and one with a single argument of the given type (in this case `succ`). +and one with a single argument of the given type (in this case `suc`). As well as enabling the above shorthand, the pragma also enables a more efficient internal representation of naturals using the Haskell