From da15bc27c6173d0efe3fab9ff4253415f48647b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Nov 2020 16:02:34 -0800
Subject: [PATCH] feat: add `Zero` and `One` classes

---
 src/Init/Prelude.lean | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a7530dbb03..bb7f775052 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -340,6 +340,9 @@ inductive Nat where
   | zero : Nat
   | succ (n : Nat) : Nat
 
+instance : Inhabited Nat where
+  default := Nat.zero
+
 /- For numeric literals notation -/
 class OfNat (α : Type u) where
   ofNat : Nat → α
@@ -350,8 +353,25 @@ export OfNat (ofNat)
 instance : OfNat Nat where
   ofNat x := x
 
-instance : Inhabited Nat where
-  default := 0
+class One (α : Type u) where
+  one : α
+
+instance [OfNat α] : One α where
+  one := ofNat Nat.zero.succ
+
+class Zero (α : Type u) where
+  zero : α
+
+instance [OfNat α] : Zero α where
+  zero := ofNat Nat.zero
+
+@[defaultInstance]
+instance : One Nat where
+  one := Nat.zero.succ
+
+@[defaultInstance]
+instance : Zero Nat where
+  zero := Nat.zero
 
 class HasLessEq (α : Type u) where LessEq : α → α → Prop
 class HasLess   (α : Type u) where Less : α → α → Prop