idris-1.3.3: test/basic017/expected.out
basic017a.idr:11:8:
|
11 | append : Vect n a -> Vect m a -> Vect (n + m) a
| ^
When checking type of Main.append:
When checking an application of Main.Vect:
No such variable n
basic017a.idr:11:8:
|
11 | append : Vect n a -> Vect m a -> Vect (n + m) a
| ^
When checking type of Main.append:
When checking an application of Main.Vect:
No such variable n