on 7afa310 help sign in
Idris-dev/test/interactive002/interactive002.idr
20 lines 428 B history raw
2foo : ?foo_arg1 -> ?foo_arg2 -> ?foo_arg3 -> ?foo_ret
3foo (S a) b c = plus (a + b + c) 42
4foo Z b c = plus b c
6bar : Vect n a -> Vect m a -> ?bar_out
7bar xs ys = xs ++ ys
9myplus : ?plus_in1 -> ?plus_in2 -> ?plus_out
10myplus Z y = y
11myplus (S k) y = S (myplus k y)
13vfun : a -> Vect n a -> Vect n a -> Vect ?what a
14vfun v xs ys = v :: ys
16ifoo : ?ifoo_arg1 -> IO ?ifoo_out
17ifoo x = do putStrLn x
18 putStrLn "World"