I have Coord
function that transforms an n-dimensional size to the type of coordinates bounded by given size: Coord [2,3] = (Fin 2, Fin 3)
.
import Data.Fin
import Data.List
Size : Type
Size = List Nat
Coord : Size -> Type
Coord [] = ()
Coord s@(_ :: _) = foldr1 (,) $ map Fin s
I'd like to use show
and other functions like (==)
with Coord s
:
foo : Coord s -> String
foo x = show x
Error: While processing right hand side of foo. Can't find an implementation for Show (Coord s).
22 | foo : Coord s -> String
23 | foo x = show x
^^^^^^
Earlier I tried to implement Show (Coord s)
, but looks like it's impossible. Here is linked question about it.
You can make your own list like data type:
You can also try using
Data.Vect.Quantifiers.All
orData.List.Quantifiers.All
: