[ new ] Introduce a default interpolation for fins

buzden · Sep 26, 2024 · 985d572 · 985d572
1 parent 776e5ce
commit 985d572
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/fin-lizzie.ipkg b/fin-lizzie.ipkg
@@ -9,7 +9,8 @@ license = "Apache-2.0"
 sourcedir = "src"
 builddir = ".build"
 
-modules = Data.Fin.Lists
+modules = Data.Fin.Interpolation
+        , Data.Fin.Lists
         , Data.Fin.Map
         , Data.Fin.Minus
         , Data.Fin.Set

diff --git a/src/Data/Fin/Interpolation.idr b/src/Data/Fin/Interpolation.idr
@@ -0,0 +1,9 @@
+module Data.Fin.Interpolation
+
+import Data.Fin
+
+%default total
+
+export %defaulthint
+FromShow : Interpolation (Fin n)
+FromShow = I where [I] Interpolation (Fin n) where interpolate = show