@@ -4,28 +4,33 @@ reg003a.idr:4:13-38:
44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
55When checking type of Main.ECons:
66No such variable OddList
7+
78reg003a.idr:7:13-38:
89 |
9107 | OCons : Nat -> EvenList -> OddList
1011 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
1112When checking type of Main.OCons:
1213No such variable EvenList
14+
1315reg003a.idr:9:6:
1416 |
15179 | test : EvenList
1618 | ^
1719When checking type of Main.test:
1820No such variable EvenList
21+
1922reg006.idr:17:1-23:
2023 |
212417 | lookup k Leaf = Nothing
2225 | ~~~~~~~~~~~~~~~~~~~~~~~
2326RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
27+
2428reg007.lidr:8:3-13:
2529 |
26308 | > A.n = Z -- This is where it's at!
2731 | ~~~~~~~~~~~
2832A.n is already defined
33+
2934reg007.lidr:12:13-18:
3035 |
313612 | > hurrah = isSame
@@ -43,42 +48,50 @@ Specifically:
4348 1
4449 and
4550 0
51+
4652reg010.idr:5:3-26:
4753 |
48545 | unsafeSubst P x x px | _ = px
4955 | ~~~~~~~~~~~~~~~~~~~~~~~~
5056When checking left hand side of with block in usubst.unsafeSubst:
5157Can't match on with block in usubst.unsafeSubst warg a P x x px
58+
5259reg018a.idr:16:1-18:
5360 |
546116 | minusCoNat Z n = Z
5562 | ~~~~~~~~~~~~~~~~~~
5663conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
64+
5765reg018a.idr:21:1-42:
5866 |
596721 | loopForever = minusCoNat infinity infinity
6068 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6169conat.loopForever is possibly not total due to: conat.minusCoNat
70+
6271reg018b.idr:8:1-28:
6372 |
64738 | showB (I x) = "I" ++ showB x
6574 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6675A.showB is possibly not total due to recursive path A.showB --> A.showB
76+
6777reg018b.idr:11:1-6:
6878 |
697911 | Show B where show = showB
7080 | ~~~~~~
7181A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
82+
7283reg018c.idr:21:1-22:21:
7384 |
748521 | inf (x :: xs) with (hdtl xs)
7586 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
7687CodataTest.inf is possibly not total due to: with block in CodataTest.inf
88+
7789reg018d.idr:8:1-39:
7890 |
79918 | pull {n=Z} _ (x :: xs) = (x, xs)
8092 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8193Main.pull is not total as there are missing cases
94+
8295reg023.idr:7:5-7:
8396 |
84977 | bad = Z
@@ -90,43 +103,51 @@ Type mismatch between
90103 Nat (Type of 0)
91104and
92105 f Nat (Expected type)
106+
93107reg028.idr:5:1-9:
94108 |
951095 | bad Z = Z
96110 | ~~~~~~~~~
97111tbad.bad is possibly not total due to: with block in tbad.bad
112+
98113reg028a.idr:17:14-18:
99114 |
10011517 | qsortLemma = proof
101116 | ~~~~~
102117This style of tactic proof is deprecated. See %runElab for the replacement.
118+
103119reg028a.idr:11:1-14:
104120 |
10512111 | qsort' [] = []
106122 | ~~~~~~~~~~~~~~
107123tbad.qsort' is possibly not total due to: with block in tbad.qsort'
124+
108125reg034.idr:6:1-14:
109126 |
1101276 | bar xs xs Refl = Refl
111128 | ~~~~~~~~~~~~~~
112129When checking left hand side of bar:
113130Can't match on bar xs xs Refl
131+
114132reg034.idr:9:1-14:
115133 |
1161349 | foo f x x Refl = Refl
117135 | ~~~~~~~~~~~~~~
118136When checking left hand side of foo:
119137Can't match on foo f x x Refl
138+
120139reg035b.idr:8:12-38:
121140 |
1221418 | fins Z = ([] ** (finZEmpty {a=_}))
123142 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~
124143No such variable __pi_arg
144+
125145reg044.idr:4:6-10:
126146 |
1271474 | pf = proof
128148 | ~~~~~
129149This style of tactic proof is deprecated. See %runElab for the replacement.
150+
130151reg044.idr:4:4-6:13:
131152 |
1321534 | pf = proof
@@ -144,12 +165,14 @@ Specifically:
144165 b
145166 and
146167 a
168+
147169reg049.idr:2:11-14:
148170 |
1491712 | Bogus : Void
150172 | ~~~~
151173When checking constructor Main.Bogus:
152174Void is not Main.Foo
175+
153176reg049.idr:5:6-12:
154177 |
1551785 | uhOh = Bogus
@@ -158,6 +181,7 @@ When checking right hand side of uhOh with expected type
158181 Void
159182
160183No such variable Bogus
184+
161185./badbangop.idr:7:1:
162186 |
1631877 | (!) : List a -> Nat -> Maybe a
@@ -177,18 +201,21 @@ reg054.idr:18:1-17:
177201When checking left hand side of inf:
178202When checking an application of constructor Main.MkInfer:
179203 Attempting concrete match on polymorphic argument: 0
204+
180205reg054.idr:34:1-18:
181206 |
18220734 | weird {x = Char} y = '5'
183208 | ~~~~~~~~~~~~~~~~~~
184209When checking left hand side of weird:
185210No explicit types on left hand side: Char
211+
186212reg054.idr:37:1-30:
187213 |
18821437 | weird' {x = Prelude.Nat.Nat} y = Z
189215 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
190216When checking left hand side of weird':
191217No explicit types on left hand side: Nat
218+
192219reg054.idr:40:1-7:
193220 |
19422140 | tctrick (Just x) = x
@@ -199,18 +226,21 @@ When checking an application of Main.tctrick:
199226 Maybe a1 (Type of Just x)
200227 and
201228 a (Expected type)
229+
202230reg055.idr:5:1-7:
203231 |
2042325 | g (f Z) = 1
205233 | ~~~~~~~
206234When checking left hand side of g:
207235Can't match on g (f 0)
236+
208237reg055.idr:8:1-5:
209238 |
2102398 | h x x = x
211240 | ~~~~~
212241When checking left hand side of h:
213242Can't match on h x x
243+
214244reg055a.idr:8:1-18:
215245 |
2162468 | foo (CAny Nothing) = 42
@@ -218,56 +248,66 @@ reg055a.idr:8:1-18:
218248When checking left hand side of foo:
219249When checking an application of constructor Foo.CAny:
220250 Attempting concrete match on polymorphic argument: Nothing
251+
221252reg055a.idr:13:1-23:
222253 |
22325413 | apply (\x => \y => x) a = a
224255 | ~~~~~~~~~~~~~~~~~~~~~~~
225256When checking left hand side of Foo.apply:
226257Can't match on apply (\x, y => x) a
258+
227259reg056.idr:7:16-25:
228260 |
2292617 | dodgy n m Refl impossible
230262 | ~~~~~~~~~~
231263dodgy n m Refl is a valid case
264+
232265reg056.idr:10:11-20:
233266 |
23426710 | nonk Refl impossible
235268 | ~~~~~~~~~~
236269nonk Refl is a valid case
270+
237271reg068.idr:1:6-8:
238272 |
2392731 | data nat : Type where --error
240274 | ~~~
241275Main.nat has a name which may be implicitly bound.
242276This is likely to lead to problems!
277+
243278reg068.idr:2:8-10:
244279 |
2452802 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
246281 | ~~~
247282Main.ze has a name which may be implicitly bound.
248283This is likely to lead to problems!
284+
249285reg068.idr:2:8-10:
250286 |
2512872 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
252288 | ~~~
253289nat is bound as an implicit
254290 Did you mean to refer to Main.nat?
291+
255292reg068.idr:2:8-10:
256293 |
2572942 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
258295 | ~~~
259296When checking constructor Main.ze:
260297Type level variable nat is not Main.nat
298+
261299Mod.idr:11:1-22:
262300 |
26330111 | natexp k = S (natfn k)
264302 | ~~~~~~~~~~~~~~~~~~~~~~
265303public export Mod.natexp can't refer to export Mod.natfn
304+
266305reg070.idr:7:1-7:
267306 |
2683077 | Show Te where
269308 | ~~~~~~~
270309Test_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
310+
271311./reg076.idr:8:1:
272312 |
2733138 | <empty line>
@@ -298,13 +338,16 @@ When checking argument value to function Prelude.Basics.the:
298338 -0.0
299339 and
300340 0.0
341+
301342Canonicity.idr:9:1-9:
302343 |
3033449 | f Nil = 0
304345 | ~~~~~~~~~
305346Canonicity.f is not total as there are missing cases
347+
306348Canonicity.idr:12:1-20:
307349 |
30835012 | NaN = f (Cons 0 Nil)
309351 | ~~~~~~~~~~~~~~~~~~~~
310352Canonicity.NaN is possibly not total due to: Canonicity.f
353+