idris-0.9.20.1: test/interactive011/interactive011.idr
import Data.Vect data Foo = Bar | Baz instance Show Foo where append : Vect n a -> Vect m a -> Vect (n + m) a append (x :: xs) ys = ?append_rhs_2
import Data.Vect data Foo = Bar | Baz instance Show Foo where append : Vect n a -> Vect m a -> Vect (n + m) a append (x :: xs) ys = ?append_rhs_2