From e4410cfbf825dc91dc0c2457a5a69726fda60d8a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Sep 2021 16:09:18 -0700
Subject: [PATCH] chore: missing `Fin` instances

---
 src/Init/Data/Fin/Basic.lean | 3 +++
 src/Init/Data/Hashable.lean  | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 0d531d6856..ee4516150d 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -103,6 +103,9 @@ instance : HMod (Fin n) Nat (Fin n) where
 instance : OfNat (Fin (no_index (n+1))) i where
   ofNat := Fin.ofNat i
 
+instance : Inhabited (Fin (no_index (n+1))) where
+  default := 0
+
 theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index 2a9bbde985..931725006d 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -36,6 +36,9 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
+instance : Hashable (Fin n) where
+  hash v := v.val.toUInt64
+
 instance : Hashable Int where
   hash
     | Int.ofNat n => UInt64.ofNat (2 * n)