Some type driven synthesis, with not very informative types

app.idr

append : List a -> List a -> List a

{-
Main> :t append
Main.append : List a -> List a -> List a
Main> :gd 1 append -- "Generate defs for 'append' on line 1"
append xs ys = ys
----
append xs ys = xs
----
append xs ys = []
----
append [] ys = ys
append (x :: xs) ys = xs
----
append [] ys = ys
append (x :: xs) ys = ys
----
append [] ys = ys
append (x :: xs) ys = []
----
append [] ys = ys
append (x :: xs) ys = x :: append xs xs
----
append [] ys = ys
append (x :: xs) ys = x :: append xs ys --- got there in the end :)
----
append [] ys = ys
append (x :: xs) ys = x :: append xs []
----
append [] ys = ys
append (x :: xs) ys = x :: append xs (x :: xs)
----
append [] ys = ys
append (x :: xs) ys = x :: append xs (x :: ys)
----
append [] ys = ys
append (x :: xs) ys = x :: append xs [x]
----
append [] ys = ys
append (x :: xs) ys = x :: append xs (x :: (x :: xs))
----
append [] ys = ys
append (x :: xs) ys = x :: append xs (x :: (x :: ys))
.... more ....
-}