From cc1eb04846b36e5f19f207056a88a0130dc44488 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Sun, 31 Dec 2017 11:55:06 -0200
Subject: [PATCH] clean up

---
 src/Basics0.lagda  | 99 ----------------------------------------------
 src/Naturals.lagda |  1 +
 2 files changed, 1 insertion(+), 99 deletions(-)
 delete mode 100644 src/Basics0.lagda

diff --git a/src/Basics0.lagda b/src/Basics0.lagda
deleted file mode 100644
index 6c9fc714..00000000
--- a/src/Basics0.lagda
+++ /dev/null
@@ -1,99 +0,0 @@
-
----
-title     : "Basics: Functional Programming in Agda"
-layout    : page
-permalink : /Basics
----
-
-\begin{code}
-open import Data.Empty       using (⊥; ⊥-elim)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Binary.PropositionalEquality
-                             using (_≡_; refl; _≢_; trans; sym)
-\end{code}
-
-# Natural numbers
-
-\begin{code}
-data ℕ : Set where
-  zero : ℕ
-  suc : ℕ → ℕ
-{-# BUILTIN NATURAL ℕ #-}
-\end{code}
-
-\begin{code}
-congruent : ∀ {m n} → m ≡ n → suc m ≡ suc n
-congruent refl = refl
-
-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
-injective refl = refl
-
-distinct : ∀ {m} → zero ≢ suc m
-distinct ()
-\end{code}
-
-\begin{code}
-_≟_ : ∀ (m n : ℕ) → Dec (m ≡ n)
-zero ≟ zero =  yes refl
-zero ≟ suc n =  no (λ()) 
-suc m ≟ zero =  no (λ())
-suc m ≟ suc n with m ≟ n
-... | yes refl =  yes refl
-... | no p =  no (λ r → p (injective r))
-\end{code}
-
-# Addition and its properties
-
-\begin{code}
-_+_ : ℕ → ℕ → ℕ
-zero + n = n
-suc m + n = suc (m + n)
-\end{code}
-
-\begin{code}
-+-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p)
-+-assoc zero n p = refl
-+-assoc (suc m) n p rewrite +-assoc m n p = refl
-
-+-zero : ∀ m → m + zero ≡ m
-+-zero zero = refl
-+-zero (suc m) rewrite +-zero m = refl
-
-+-suc : ∀ m n → m + (suc n) ≡ suc (m + n)
-+-suc zero n = refl
-+-suc (suc m) n rewrite +-suc m n = refl
-
-+-comm : ∀ m n → m + n ≡ n + m
-+-comm m zero =  +-zero m
-+-comm m (suc n) rewrite +-suc m n | +-comm m n = refl
-\end{code}
-
-# Equality and decidable equality for naturals
-
-
-
-
-# Showing `double` injective
-
-\begin{code}
-double : ℕ → ℕ
-double zero  =  zero
-double (suc n)  =  suc (suc (double n))
-\end{code}
-
-\begin{code}
-double-injective : ∀ m n → double m ≡ double n → m ≡ n
-double-injective zero zero refl = refl
-double-injective zero (suc n) ()
-double-injective (suc m) zero ()
-double-injective (suc m) (suc n) r =
-   congruent (double-injective m n (injective (injective r)))
-\end{code}
-
-In Coq, the inductive proof for `double-injective`
-is sensitive to how one inducts on `m` and `n`. In Agda, that aspect
-is straightforward. However, Agda requires helper functions for
-injection and congruence which are not required in Coq.
-
-I can remove the use of `congruent` by rewriting with its argument.
-Is there an easy way to remove the two uses of `injective`?
diff --git a/src/Naturals.lagda b/src/Naturals.lagda
index 261cafa7..351e44f2 100644
--- a/src/Naturals.lagda
+++ b/src/Naturals.lagda
@@ -12,6 +12,7 @@ But the number of stars is finite, while natural numbers are infinite.
 Count all the stars, and you will still have as many natural numbers
 left over as you started with.
 
+
 ## The naturals are an inductive datatype
 
 Everyone is familiar with the natural numbers: