[ fix ] missing Show (Fin n) in base

idris-lang · Jun 23, 2021 · afd5595 · afd5595
1 parent 4d12766
commit afd5595
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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