Skip to content

Commit afd5595

Browse files
committed
[ fix ] missing Show (Fin n) in base
1 parent 4d12766 commit afd5595

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

libs/base/Data/Fin.idr

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,11 @@ finToNat : Fin n -> Nat
5656
finToNat FZ = Z
5757
finToNat (FS k) = S $ finToNat k
5858

59+
60+
export
61+
Show (Fin n) where
62+
show = show . finToNat
63+
5964
||| `finToNat` is injective
6065
export
6166
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn

0 commit comments

Comments
 (0)