idris-0.10: test/interactive011/interactive011.idr

import Data.Vect

data Foo = Bar | Baz

implementation Show Foo where

append : Vect n a -> Vect m a -> Vect (n + m) a
append (x :: xs) ys = ?append_rhs_2