0 | module Data.Fin.Interpolation 1 | 2 | import public Data.Fin 3 | 4 | %default total 5 | 6 | export %defaulthint 7 | FromShow : Interpolation (Fin n) 8 | FromShow = I where [I] Interpolation (Fin n) where interpolate = show 9 |