git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/basic006/test020.idr
27 lines 398 B history raw
1module Main
3import Data.Vect
5implicit
6natInt : Nat -> Integer
7natInt x = cast x
9implicit
10forget : Vect n a -> List a
11forget [] = []
12forget (x :: xs) = x :: forget xs
14foo : Vect n a -> List a
15foo xs = reverse xs
17implicit intString : Integer -> String
18intString = show
20test : Integer -> String
21test x = "Number " ++ x
23main : IO ()
24main = do printLn (foo [1,2,3])
25 printLn (test 42)