git.iko.soy/Idris-dev
on b56ef01 help sign in
Idris-dev/test/error006/expected
21 lines 552 B history raw
1WithPatsNoWith.idr:4:1-13:
2 |
34 | foo 1 | 2 | 3 = True
4 | ~~~~~~~~~~~~~
5When checking left hand side of foo:
6unexpected patterns outside of "with" block
8WithPatsNoWith.idr:9:3-16:
9 |
109 | foo2 n | 1 | 2 = True
11 | ~~~~~~~~~~~~~~
12When checking left hand side of with block in WithPatsNoWith.foo2:
13unexpected extra "with" patterns
15WithPatsNoWith.idr:15:5-24:
16 |
1715 | foo3 _ _ | 2 | 3 | 4 = True
18 | ~~~~~~~~~~~~~~~~~~~~
19When checking left hand side of with block in with block in WithPatsNoWith.foo3:
20unexpected extra "with" patterns