git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/test/layout001/expected
73 lines 1.4 kB history raw
1./layout001a.idr:5:1:
2 |
35 | y
4 | ^
5Wrong indention: should be greater than context indentation
7./layout001b.idr:5:3:
8 |
95 | = y
10 | ^
11Wrong indention: should be greater than context indentation
13./layout001c.idr:3:1:
14 |
153 | 2
16 | ^
17= is not a valid operator
18Wrong indention: should be greater than context indentation
20./layout001e.idr:6:1:
21 |
226 | 3
23 | ^
24Wrong indention: should be greater than context indentation
26./layout001f.idr:6:2:
27 |
286 | 3
29 | ^
30Wrong indention: should be greater than context indentation
32./layout001g.idr:6:3:
33 |
346 | 3
35 | ^
36Wrong indention: should be greater than context indentation
38./layout001h.idr:6:3:
39 |
406 | 3
41 | ^
42Wrong indention: should be greater than context indentation
44./layout001i.idr:6:4:
45 |
466 | 3
47 | ^
48Wrong indention: should be greater than context indentation
50./layout001j.idr:6:5:
51 |
526 | 3
53 | ^
54Wrong indention: should be greater than context indentation
56./layout001l.idr:6:1:
57 |
586 | y
59 | ^
60Wrong indention: should be greater than context indentation
62mplus1.idr:13:31:When checking right hand side of term with expected type
63 Maybe Int
65When checking an application of function Prelude.Applicative.pure:
66 No such variable f
67./mplus2.idr:17:37:
68 |
6917 | `mplus` pure f
70 | ^
71not end of block
73mplus3.idr:11:1:warning - Unreachable case: term