@@ -1,6 +1,6 @@
1−reg001.idr:3:1-9:
1+reg001.idr:2:1-9:
3−3 | foo a a x = x
3+2 | foo a a x = x
4 | ~~~~~~~~~
4 | ~~~~~~~~~
5When checking left hand side of foo:
5When checking left hand side of foo:
6Can't match on foo a a x
6Can't match on foo a a x
@@ -87,274 +87,3 @@ reg018b.idr:11:1-6:
88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
90−reg018c.idr:21:1-22:21:
92−21 | inf (x :: xs) with (hdtl xs)
93− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
94−CodataTest.inf is possibly not total due to: with block in CodataTest.inf
98−8 | pull {n=Z} _ (x :: xs) = (x, xs)
99− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
100−Main.pull is not total as there are missing cases
106−When checking right hand side of bad with expected type
109−Type mismatch between
112− f Nat (Expected type)
118−tbad.bad is possibly not total due to: with block in tbad.bad
120−reg028a.idr:17:14-18:
122−17 | qsortLemma = proof
124−This style of tactic proof is deprecated. See %runElab for the replacement.
130−tbad.qsort' is possibly not total due to: with block in tbad.qsort'
134−6 | bar xs xs Refl = Refl
136−When checking left hand side of bar:
137−Can't match on bar xs xs Refl
141−9 | foo f x x Refl = Refl
143−When checking left hand side of foo:
144−Can't match on foo f x x Refl
148−8 | fins Z = ([] ** (finZEmpty {a=_}))
149− | ~~~~~~~~~~~~~~~~~~~~~~~~~
150−No such variable __pi_arg
156−This style of tactic proof is deprecated. See %runElab for the replacement.
162−When checking right hand side of Main.pf with expected type
163− (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
165−Type mismatch between
166− b = b (Type of Refl)
168− a = b (Expected type)
171− Type mismatch between
180−When checking constructor Main.Bogus:
187−When checking right hand side of uhOh with expected type
190−No such variable Bogus
194−7 | (!) : List a -> Nat -> Maybe a
196−! is not a valid operator
198−baddoublebang.idr:6:28:
200−6 | doubleBang mmn = do pure !!mmn
202−unexpected Operator without known fixity: !!
206−18 | inf (MkInfer _ Z) = True
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
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
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
228−40 | tctrick (Just x) = x
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)
241−When checking left hand side of g:
242−Can't match on g (f 0)
248−When checking left hand side of h:
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
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
268−7 | dodgy n m Refl impossible
270−dodgy n m Refl is a valid case
274−10 | nonk Refl impossible
276−nonk Refl is a valid case
280−1 | data nat : Type where --error
282−Main.nat has a name which may be implicitly bound.
283−This is likely to lead to problems!
287−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
289−Main.ze has a name which may be implicitly bound.
290−This is likely to lead to problems!
294−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
296−nat is bound as an implicit
297− Did you mean to refer to Main.nat?
301−2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
303−When checking constructor Main.ze:
304−Type level variable nat is not Main.nat
308−11 | natexp k = S (natfn k)
309− | ~~~~~~~~~~~~~~~~~~~~~~
310−public export Mod.natexp can't refer to export Mod.natfn
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
322−Missing fixity declaration for Main.:>
328−Missing fixity declaration for Main.:>>
330−DoubleEquality.idr:4:83-103:
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
337−When checking argument value to function Prelude.Basics.the:
338− Type mismatch between
339− x = x (Type of Refl)
341− (-0.0) = 0.0 (Expected type)
344− Type mismatch between
349−Canonicity.idr:9:1-9:
353−Canonicity.f is not total as there are missing cases
355−Canonicity.idr:12:1-20:
357−12 | NaN = f (Cons 0 Nil)
358− | ~~~~~~~~~~~~~~~~~~~~
359−Canonicity.NaN is possibly not total due to: Canonicity.f