git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/test/delab001/expected
12 lines 315 B history raw
1foo : Nat -> String
2foo n = case n of
3 0 => "z"
4 S _ => "s"
5bar : Nat -> String -> String
6bar x y = case x of
7 0 => y
8 S _ => (y ++ y)
9append : List a -> List a -> List a
10append xs ys = case xs of
11 [] => ys
12 (x :: xs) => (x :: (append xs ys))