From afd55951c25c5327059180b1fd74a980ad83e910 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Wed, 23 Jun 2021 16:46:25 +0100
Subject: [PATCH] [ fix ] missing Show (Fin n) in base

---
 libs/base/Data/Fin.idr | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index e4f7e5ae9d..1a4016118c 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -56,6 +56,11 @@ finToNat : Fin n -> Nat
 finToNat FZ = Z
 finToNat (FS k) = S $ finToNat k
 
+
+export
+Show (Fin n) where
+  show = show . finToNat
+
 ||| `finToNat` is injective
 export
 finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn