expected

foo : Nat -> String
foo n = case n of
          0 => "z"
          S _ => "s"
bar : Nat -> String -> String
bar x y = case x of
            0 => y
            S _ => (y ++ y)
append : List a -> List a -> List a
append xs ys = case xs of
                 [] => ys
                 (x :: xs) => (x :: (append xs ys))