on fdfd99e help sign in
Idris-dev/test/interactive011/interactive011.idr
11 lines 158 B history raw
1import Data.Vect
3data Foo = Bar | Baz
5implementation Show Foo where
7append : Vect n a -> Vect m a -> Vect (n + m) a
8append (x :: xs) ys = ?append_rhs_2