git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/test/regression002/expected
150 lines 5.3 kB history raw
1reg003a.idr:4:11:When checking type of Main.ECons:
2No such variable OddList
3reg003a.idr:7:11:When checking type of Main.OCons:
4No such variable EvenList
5reg003a.idr:9:6:When checking type of Main.test:
6No such variable EvenList
7reg006.idr:17:1:
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
9reg007.lidr:8:3:A.n is already defined
10reg007.lidr:12:13-19:When checking right hand side of hurrah with expected type
11 0 = 1
13Type mismatch between
14 n = lala (Type of isSame)
15and
16 0 = 1 (Expected type)
18Specifically:
19 Type mismatch between
20 1
21 and
22 0
23reg010.idr:5:15:
24When checking left hand side of with block in usubst.unsafeSubst:
25Can't match on with block in usubst.unsafeSubst warg a P x x px
26reg018a.idr:16:1:
27conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
28reg018a.idr:21:1:
29conat.loopForever is possibly not total due to: conat.minusCoNat
30reg018b.idr:8:1:
31A.showB is possibly not total due to recursive path A.showB --> A.showB
32reg018b.idr:11:1:
33A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
34reg018c.idr:21:1:
35CodataTest.inf is possibly not total due to: with block in CodataTest.inf
36reg018d.idr:8:1:Main.pull is not total as there are missing cases
37reg023.idr:7:5:When checking right hand side of bad with expected type
38 f Nat
40Type mismatch between
41 Nat (Type of 0)
42and
43 f Nat (Expected type)
44reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad
45reg028a.idr:17:14-19:
46This style of tactic proof is deprecated. See %runElab for the replacement.
47reg028a.idr:11:1:
48tbad.qsort' is possibly not total due to: with block in tbad.qsort'
49reg034.idr:6:5:When checking left hand side of bar:
50Can't match on bar xs xs Refl
51reg034.idr:9:5:When checking left hand side of foo:
52Can't match on foo f x x Refl
53reg035b.idr:8:6:No such variable __pi_arg
54reg044.idr:4:6-11:
55This style of tactic proof is deprecated. See %runElab for the replacement.
56reg044.idr:4:4:When checking right hand side of Main.pf with expected type
57 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
59Type mismatch between
60 b = b (Type of Refl)
61and
62 a = b (Expected type)
64Specifically:
65 Type mismatch between
66 b
67 and
68 a
69reg049.idr:2:9:When checking constructor Main.Bogus:
70Void is not Main.Foo
71reg049.idr:5:6:When checking right hand side of uhOh with expected type
72 Void
74No such variable Bogus
75./badbangop.idr:7:1:
76 |
777 | (!) : List a -> Nat -> Maybe a
78 | ^
79! is not a valid operator
81./baddoublebang.idr:6:28:
82 |
836 | doubleBang mmn = do pure !!mmn
84 | ^
85unexpected Operator without known fixity: !!
87reg054.idr:18:5:When checking left hand side of inf:
88When checking an application of constructor Main.MkInfer:
89 Attempting concrete match on polymorphic argument: 0
90reg054.idr:34:7:When checking left hand side of weird:
91No explicit types on left hand side: Char
92reg054.idr:37:8:When checking left hand side of weird':
93No explicit types on left hand side: Nat
94reg054.idr:40:1-8:When checking left hand side of tctrick:
95When checking an application of Main.tctrick:
96 Type mismatch between
97 Maybe a1 (Type of Just x)
98 and
99 a (Expected type)
100reg055.idr:5:3:When checking left hand side of g:
101Can't match on g (f 0)
102reg055.idr:8:3:When checking left hand side of h:
103Can't match on h x x
104reg055a.idr:8:5:When checking left hand side of foo:
105When checking an application of constructor Foo.CAny:
106 Attempting concrete match on polymorphic argument: Nothing
107reg055a.idr:13:7:When checking left hand side of Foo.apply:
108Can't match on apply (\x, y => x) a
109reg056.idr:7:7:dodgy n m Refl is a valid case
110reg056.idr:10:6:nonk Refl is a valid case
111reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
112This is likely to lead to problems!
113reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
114This is likely to lead to problems!
115reg068.idr:2:8-11:
116nat is bound as an implicit
117 Did you mean to refer to Main.nat?
118reg068.idr:2:6:When checking constructor Main.ze:
119Type level variable nat is not Main.nat
120Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn
121reg070.idr:7:1:
122Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
123./reg076.idr:8:1:
124 |
1258 | <empty line>
126 | ^
127Missing fixity declaration for Main.:>
129./reg077.idr:3:1:
130 |
1313 | <empty line>
132 | ^
133Missing fixity declaration for Main.:>>
135DoubleEquality.idr:4:87:When checking right hand side of oops with expected type
136 Void
138When checking argument value to function Prelude.Basics.the:
139 Type mismatch between
140 x = x (Type of Refl)
141 and
142 (-0.0) = 0.0 (Expected type)
144 Specifically:
145 Type mismatch between
146 -0.0
147 and
148 0.0
149Canonicity.idr:9:1:Canonicity.f is not total as there are missing cases
150Canonicity.idr:12:1:Canonicity.NaN is possibly not total due to: Canonicity.f