Idris2/tests/idris2/error001/Error.idr

mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

wrong : a -> Vect (S n) a -> Vect (S n) a
wrong x xs = x :: x
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`data Vect : Nat -> Type -> Type where`
			`Nil : Vect Z a`
			`(::) : a -> Vect k a -> Vect (S k) a`

			`wrong : a -> Vect (S n) a -> Vect (S n) a`
			`wrong x xs = x :: x`