git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/basic006/test020a.idr
18 lines 272 B history raw
1module Main
3implicit
4forget : Vect n a -> List a
5forget [] = []
6forget (x :: xs) = x :: forget xs
8implicit
9forget' : Vect n a -> List a
10forget' [] = []
11forget' (x :: xs) = forget xs
13foo : Vect n a -> List a
14foo xs = reverse xs
16main : IO ()
17main = print (foo [1,2,3])