Merge pull request #1598 from gallais/show-void

[ fix ] missing Show implementations in libs

Author: edwinb

libs/base/Data/Fin.idr

@@ -60,6 +60,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

libs/prelude/Prelude/Show.idr

@@ -179,6 +179,10 @@ Show Bool where
   show True = "True"
   show False = "False"
 
+export
+Show Void where
+  show v impossible
+
 export
 Show () where
   show () = "()"

tests/idris2/docs001/expected

@@ -51,6 +51,7 @@ Main> Prelude.Show : Type -> Type
     Show String
     Show Nat
     Show Bool
+    Show Void
     Show ()
     (Show a, Show b) => Show (a, b)
     (Show a, Show (p y)) => Show (DPair a p)