Merge pull request #1598 from gallais/show-void

[ fix ] missing Show implementations in libs
idris-lang · Jun 23, 2021 · 5689786 · 5689786
2 parents 0a0c41d + afd5595
commit 5689786
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git a/libs/base/Data/Fin.idr b/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

diff --git a/libs/prelude/Prelude/Show.idr b/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 () = "()"

diff --git a/tests/idris2/docs001/expected b/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)