From a83e020034ca1ff4c9075518d03deb68e607d0b9 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Fri, 29 Dec 2017 14:54:12 -0200
Subject: [PATCH] first draft of Naturals

---
 index.md           |  1 +
 src/Naturals.lagda | 66 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 src/Naturals.lagda

diff --git a/index.md b/index.md
index 750defcf..40e349ba 100644
--- a/index.md
+++ b/index.md
@@ -21,6 +21,7 @@ http://homepages.inf.ed.ac.uk/wadler/
   - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
 -->
 
+  - [Naturals: Natural numbers]({{ "/Naturals" | relative_rul }})
   - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
   - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
   - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
diff --git a/src/Naturals.lagda b/src/Naturals.lagda
new file mode 100644
index 00000000..323109ec
--- /dev/null
+++ b/src/Naturals.lagda
@@ -0,0 +1,66 @@
+---
+title     : "Naturals: Natural numbers"
+layout    : page
+permalink : /Naturals
+---
+
+... introduction ...
+
+## The naturals are an inductive datatype
+
+Our first example of an inductive datatype is ℕ, the natural numbers.
+\begin{code}
+data ℕ : Set where
+  zero : ℕ
+  suc  : ℕ → ℕ
+\end{code}
+Here `ℕ` is the name of the *datatype* we are creating,
+and `zero` and `suc` (short for successor) are the
+*constructors* of the datatype.
+
+Let's unpack this definition. The keyword `data` tells us this is an
+inductive definition, that is, that we are defining a new datatype
+with constructors.  The phrase
+
+    ℕ : Set
+
+tells us that `ℕ` is the name of the new datatype, and that it is a
+`Set`, which is the way in Agda of saying that it is a type.  The
+keyword `where` separates the declaration of the datatype from the
+declaration of its constructors. Each constructor is declared on a
+separate line, which is indented to indicate that it belongs to the
+corresponding `data` declaration.  The lines
+
+    zero : ℕ
+    suc : ℕ → ℕ
+
+tell us that `zero` is a natural number and that `suc` takes a natural
+number as argument and returns a natural number.
+
+Here `ℕ` and `→` are special symbols, meaning that you won't find them
+on your keyboard. At the end of each chapter is a list of all the
+special symbols, including instructions on how to type them in the
+Emacs text editor.
+
+### Pragmas
+
+\begin{code}
+{-# BUILTIN NATURAL ℕ #-}
+\end{code}
+
+## Operations on naturals are recursive functions
+
+## Equality on naturals is also an inductive datatype
+
+## Proofs over naturals are also recursive functions
+
+
+## Special characters
+
+In each chapter, we will list all special characters used at the end.
+In this chapter we use the following special characters.
+
+    ℕ  U+2115:  DOUBLE-STRUCK CAPITAL N (\bN)  
+    →  U+2192:  RIGHTWARDS ARROW (\to, \r) 
+    ∀  U+2200:  FOR ALL (\forall)
+    λ  U+03BB:  GREEK SMALL LETTER LAMBDA (\Gl, \lambda)