5When checking left hand side of foo:
6Can't match on foo a a x
103 | append (X :: XS) ys = X :: append XS ys
12When checking left hand side of append:
13When checking argument x to constructor Prelude.List.:::
14 X is not a valid name for a pattern variable
184 | ECons : Nat -> OddList -> EvenList
19 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
20When checking type of Main.ECons:
21No such variable OddList
257 | OCons : Nat -> EvenList -> OddList
26 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
27When checking type of Main.OCons:
28No such variable EvenList
34When checking type of Main.test:
35No such variable EvenList
3917 | lookup k Leaf = Nothing
40 | ~~~~~~~~~~~~~~~~~~~~~~~
41RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
458 | > A.n = Z -- This is where it's at!
53When checking right hand side of hurrah with expected type
57 n = lala (Type of isSame)
695 | unsafeSubst P x x px | _ = px
70 | ~~~~~~~~~~~~~~~~~~~~~~~~
71When checking left hand side of with block in usubst.unsafeSubst:
72Can't match on with block in usubst.unsafeSubst warg a P x x px
7616 | minusCoNat Z n = Z
78conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
8221 | loopForever = minusCoNat infinity infinity
83 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
84conat.loopForever is possibly not total due to: conat.minusCoNat
888 | showB (I x) = "I" ++ showB x
89 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
90A.showB is possibly not total due to recursive path A.showB --> A.showB
9411 | Show B where show = showB
96A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
98reg018c.idr:21:1-22:21:
10021 | inf (x :: xs) with (hdtl xs)
101 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
102CodataTest.inf is possibly not total due to: with block in CodataTest.inf
1068 | pull {n=Z} _ (x :: xs) = (x, xs)
107 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
108Main.pull is not total as there are missing cases
114When checking right hand side of bad with expected type
120 f Nat (Expected type)
126tbad.bad is possibly not total due to: with block in tbad.bad
13017 | qsortLemma = proof
132This style of tactic proof is deprecated. See %runElab for the replacement.
138tbad.qsort' is possibly not total due to: with block in tbad.qsort'
1426 | bar xs xs Refl = Refl
144When checking left hand side of bar:
145Can't match on bar xs xs Refl
1499 | foo f x x Refl = Refl
151When checking left hand side of foo:
152Can't match on foo f x x Refl
1568 | fins Z = ([] ** (finZEmpty {a=_}))
157 | ~~~~~~~~~~~~~~~~~~~~~~~~~
158No such variable __pi_arg
164This style of tactic proof is deprecated. See %runElab for the replacement.
170When checking right hand side of Main.pf with expected type
171 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
176 a = b (Expected type)
179 Type mismatch between
188When checking constructor Main.Bogus:
195When checking right hand side of uhOh with expected type
198No such variable Bogus
2027 | (!) : List a -> Nat -> Maybe a
204! is not a valid operator
206baddoublebang.idr:6:28:
2086 | doubleBang mmn = do pure !!mmn
210unexpected Operator without known fixity: !!
21418 | inf (MkInfer _ Z) = True
216When checking left hand side of inf:
217When checking an application of constructor Main.MkInfer:
218 Attempting concrete match on polymorphic argument: 0
22234 | weird {x = Char} y = '5'
224When checking left hand side of weird:
225No explicit types on left hand side: Char
22937 | weird' {x = Prelude.Nat.Nat} y = Z
230 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
231When checking left hand side of weird':
232No explicit types on left hand side: Nat
23640 | tctrick (Just x) = x
238When checking left hand side of tctrick:
239When checking an application of Main.tctrick:
240 Type mismatch between
241 Maybe a1 (Type of Just x)
249When checking left hand side of g:
250Can't match on g (f 0)
256When checking left hand side of h:
2618 | foo (CAny Nothing) = 42
263When checking left hand side of foo:
264When checking an application of constructor Foo.CAny:
265 Attempting concrete match on polymorphic argument: Nothing
26913 | apply (\x => \y => x) a = a
270 | ~~~~~~~~~~~~~~~~~~~~~~~
271When checking left hand side of Foo.apply:
272Can't match on apply (\x, y => x) a
2767 | dodgy n m Refl impossible
278dodgy n m Refl is a valid case
28210 | nonk Refl impossible
284nonk Refl is a valid case
2881 | data nat : Type where --error
290Main.nat has a name which may be implicitly bound.
291This is likely to lead to problems!
2952 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
297Main.ze has a name which may be implicitly bound.
298This is likely to lead to problems!
3022 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
304nat is bound as an implicit
305 Did you mean to refer to Main.nat?
3092 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
311When checking constructor Main.ze:
312Type level variable nat is not Main.nat
31611 | natexp k = S (natfn k)
317 | ~~~~~~~~~~~~~~~~~~~~~~
318public export Mod.natexp can't refer to export Mod.natfn
324Test_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
330Missing fixity declaration for Main.:>
336Missing fixity declaration for Main.:>>
338DoubleEquality.idr:4:83-103:
3404 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
341 | ~~~~~~~~~~~~~~~~~~~~~
342When checking right hand side of oops with expected type
345When checking argument value to function Prelude.Basics.the:
346 Type mismatch between
349 -0.0 = 0.0 (Expected type)
352 Type mismatch between
361Canonicity.f is not total as there are missing cases
363Canonicity.idr:12:1-20:
36512 | NaN = f (Cons 0 Nil)
366 | ~~~~~~~~~~~~~~~~~~~~
367Canonicity.NaN is possibly not total due to: Canonicity.f
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list