git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/basic006/test020.idr
25 lines 376 B history raw
1module Main
3implicit
4natInt : Nat -> Integer
5natInt x = cast x
7implicit
8forget : Vect n a -> List a
9forget [] = []
10forget (x :: xs) = x :: forget xs
12foo : Vect n a -> List a
13foo xs = reverse xs
15implicit intString : Integer -> String
16intString = show
18test : Integer -> String
19test x = "Number " ++ x
21main : IO ()
22main = do print (foo [1,2,3])
23 print (test 42)