From 964ed65922182afba5ab4cb30fc9220e3bd97ca9 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Sun, 1 Oct 2017 22:06:35 +0100
Subject: [PATCH] decidable equality in basics

---
 src/Basics.lagda | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Basics.lagda b/src/Basics.lagda
index 815d1bf9..6c9fc714 100644
--- a/src/Basics.lagda
+++ b/src/Basics.lagda
@@ -18,6 +18,7 @@ open import Relation.Binary.PropositionalEquality
 data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ
+{-# BUILTIN NATURAL ℕ #-}
 \end{code}
 
 \begin{code}
@@ -31,6 +32,16 @@ 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}