git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/basic006/test020a.idr
20 lines 292 B history raw
1module Main
3import Data.Vect
5implicit
6forget : Vect n a -> List a
7forget [] = []
8forget (x :: xs) = x :: forget xs
10implicit
11forget' : Vect n a -> List a
12forget' [] = []
13forget' (x :: xs) = forget xs
15foo : Vect n a -> List a
16foo xs = reverse xs
18main : IO ()
19main = printLn (foo [1,2,3])