on master help sign in
Idris-dev/test/basic017/expected.out
8 lines 198 B history raw
1basic017a.idr:11:8:
2 |
311 | append : Vect n a -> Vect m a -> Vect (n + m) a
4 | ^
5When checking type of Main.append:
6When checking an application of Main.Vect:
7 No such variable n