@@ -1,6 +1,6 @@
1−reg001.idr:3:1-9:
1+reg001.idr:2:1-9:
22 |
3−3 | foo a a x = x
3+2 | foo a a x = x
44 | ~~~~~~~~~
55When checking left hand side of foo:
66Can't match on foo a a x
@@ -87,274 +87,3 @@ reg018b.idr:11:1-6:
8787 | ~~~~~~
8888A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
8989
90−reg018c.idr:21:1-22:21:
91− |
92−21 | inf (x :: xs) with (hdtl xs)
93− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
94−CodataTest.inf is possibly not total due to: with block in CodataTest.inf
95−
96−reg018d.idr:8:1-39:
97− |
98−8 | pull {n=Z} _ (x :: xs) = (x, xs)
99− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
100−Main.pull is not total as there are missing cases
101−
102−reg023.idr:7:7:
103− |
104−7 | bad = Z
105− | ^
106−When checking right hand side of bad with expected type
107− f Nat
108−
109−Type mismatch between
110− Nat (Type of 0)
111−and
112− f Nat (Expected type)
113−
114−reg028.idr:5:1-9:
115− |
116−5 | bad Z = Z
117− | ~~~~~~~~~
118−tbad.bad is possibly not total due to: with block in tbad.bad
119−
120−reg028a.idr:17:14-18:
121− |
122−17 | qsortLemma = proof
123− | ~~~~~
124−This style of tactic proof is deprecated. See %runElab for the replacement.
125−
126−reg028a.idr:11:1-14:
127− |
128−11 | qsort' [] = []
129− | ~~~~~~~~~~~~~~
130−tbad.qsort' is possibly not total due to: with block in tbad.qsort'
131−
132−reg034.idr:6:1-14:
133− |
134−6 | bar xs xs Refl = Refl
135− | ~~~~~~~~~~~~~~
136−When checking left hand side of bar:
137−Can't match on bar xs xs Refl
138−
139−reg034.idr:9:1-14:
140− |
141−9 | foo f x x Refl = Refl
142− | ~~~~~~~~~~~~~~
143−When checking left hand side of foo:
144−Can't match on foo f x x Refl
145−
146−reg035b.idr:8:14-38:
147− |
148−8 | fins Z = ([] ** (finZEmpty {a=_}))
149− | ~~~~~~~~~~~~~~~~~~~~~~~~~
150−No such variable __pi_arg
151−
152−reg044.idr:4:6-10:
153− |
154−4 | pf = proof
155− | ~~~~~
156−This style of tactic proof is deprecated. See %runElab for the replacement.
157−
158−reg044.idr:4:6-6:13:
159− |
160−4 | pf = proof
161− | ~~~~~ ...
162−When checking right hand side of Main.pf with expected type
163− (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
164−
165−Type mismatch between
166− b = b (Type of Refl)
167−and
168− a = b (Expected type)
169−
170−Specifically:
171− Type mismatch between
172− b
173− and
174− a
175−
176−reg049.idr:2:11-14:
177− |
178−2 | Bogus : Void
179− | ~~~~
180−When checking constructor Main.Bogus:
181−Void is not Main.Foo
182−
183−reg049.idr:5:8-12:
184− |
185−5 | uhOh = Bogus
186− | ~~~~~
187−When checking right hand side of uhOh with expected type
188− Void
189−
190−No such variable Bogus
191−
192−badbangop.idr:7:1:
193− |
194−7 | (!) : List a -> Nat -> Maybe a
195− | ^
196−! is not a valid operator
197−
198−baddoublebang.idr:6:28:
199− |
200−6 | doubleBang mmn = do pure !!mmn
201− | ^
202−unexpected Operator without known fixity: !!
203−
204−reg054.idr:18:1-17:
205− |
206−18 | inf (MkInfer _ Z) = True
207− | ~~~~~~~~~~~~~~~~~
208−When checking left hand side of inf:
209−When checking an application of constructor Main.MkInfer:
210− Attempting concrete match on polymorphic argument: 0
211−
212−reg054.idr:34:1-18:
213− |
214−34 | weird {x = Char} y = '5'
215− | ~~~~~~~~~~~~~~~~~~
216−When checking left hand side of weird:
217−No explicit types on left hand side: Char
218−
219−reg054.idr:37:1-30:
220− |
221−37 | weird' {x = Prelude.Nat.Nat} y = Z
222− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223−When checking left hand side of weird':
224−No explicit types on left hand side: Nat
225−
226−reg054.idr:40:1-7:
227− |
228−40 | tctrick (Just x) = x
229− | ~~~~~~~
230−When checking left hand side of tctrick:
231−When checking an application of Main.tctrick:
232− Type mismatch between
233− Maybe a1 (Type of Just x)
234− and
235− a (Expected type)
236−
237−reg055.idr:5:1-7:
238− |
239−5 | g (f Z) = 1
240− | ~~~~~~~
241−When checking left hand side of g:
242−Can't match on g (f 0)
243−
244−reg055.idr:8:1-5:
245− |
246−8 | h x x = x
247− | ~~~~~
248−When checking left hand side of h:
249−Can't match on h x x
250−
251−reg055a.idr:8:1-18:
252− |
253−8 | foo (CAny Nothing) = 42
254− | ~~~~~~~~~~~~~~~~~~
255−When checking left hand side of foo:
256−When checking an application of constructor Foo.CAny:
257− Attempting concrete match on polymorphic argument: Nothing
258−
259−reg055a.idr:13:1-23:
260− |
261−13 | apply (\x => \y => x) a = a
262− | ~~~~~~~~~~~~~~~~~~~~~~~
263−When checking left hand side of Foo.apply:
264−Can't match on apply (\x, y => x) a
265−
266−reg056.idr:7:16-25:
267− |
268−7 | dodgy n m Refl impossible
269− | ~~~~~~~~~~
270−dodgy n m Refl is a valid case
271−
272−reg056.idr:10:11-20:
273− |
274−10 | nonk Refl impossible
275− | ~~~~~~~~~~
276−nonk Refl is a valid case
277−
278−reg068.idr:1:6-8:
279− |
280−1 | data nat : Type where --error
281− | ~~~
282−Main.nat has a name which may be implicitly bound.
283−This is likely to lead to problems!
284−
285−reg068.idr:2:8-10:
286− |
287−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
288− | ~~~
289−Main.ze has a name which may be implicitly bound.
290−This is likely to lead to problems!
291−
292−reg068.idr:2:8-10:
293− |
294−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
295− | ~~~
296−nat is bound as an implicit
297− Did you mean to refer to Main.nat?
298−
299−reg068.idr:2:8-10:
300− |
301−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
302− | ~~~
303−When checking constructor Main.ze:
304−Type level variable nat is not Main.nat
305−
306−Mod.idr:11:1-22:
307− |
308−11 | natexp k = S (natfn k)
309− | ~~~~~~~~~~~~~~~~~~~~~~
310−public export Mod.natexp can't refer to export Mod.natfn
311−
312−reg070.idr:7:1-7:
313− |
314−7 | Show Te where
315− | ~~~~~~~
316−Test_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
317−
318−reg076.idr:8:1:
319− |
320−8 | <end of file>
321− | ^
322−Missing fixity declaration for Main.:>
323−
324−reg077.idr:3:1:
325− |
326−3 | <end of file>
327− | ^
328−Missing fixity declaration for Main.:>>
329−
330−DoubleEquality.idr:4:83-103:
331− |
332−4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
333− | ~~~~~~~~~~~~~~~~~~~~~
334−When checking right hand side of oops with expected type
335− Void
336−
337−When checking argument value to function Prelude.Basics.the:
338− Type mismatch between
339− x = x (Type of Refl)
340− and
341− (-0.0) = 0.0 (Expected type)
342−
343− Specifically:
344− Type mismatch between
345− -0.0
346− and
347− 0.0
348−
349−Canonicity.idr:9:1-9:
350− |
351−9 | f Nil = 0
352− | ~~~~~~~~~
353−Canonicity.f is not total as there are missing cases
354−
355−Canonicity.idr:12:1-20:
356− |
357−12 | NaN = f (Cons 0 Nil)
358− | ~~~~~~~~~~~~~~~~~~~~
359−Canonicity.NaN is possibly not total due to: Canonicity.f
360−