git.iko.soy/Idris-dev
on 229331c help sign in
Idris-dev/test/syntax001/expected
26 lines 644 B history raw
1Syntax.idr:6:7-18:
2 |
36 | foo = fnord "argh"
4 | ~~~~~~~~~~~~
5When checking right hand side of foo with expected type
6 Nat
8When checking an application of function Prelude.Interfaces.+:
9 Type mismatch between
10 String (Type of "argh")
11 and
12 Nat (Expected type)
14SyntaxTest.idr:5:7-18:
15 |
165 | foo = fnord "argh"
17 | ~~~~~~~~~~~~
18When checking right hand side of foo with expected type
19 Nat
21When checking an application of function Prelude.Interfaces.+:
22 Type mismatch between
23 String (Type of "argh")
24 and
25 Nat (Expected type)