reg003a.idr:4:13-38:
|
4 | ECons : Nat -> OddList -> EvenList
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking type of Main.ECons:
No such variable OddList
reg003a.idr:7:13-38:
|
7 | OCons : Nat -> EvenList -> OddList
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking type of Main.OCons:
No such variable EvenList
reg003a.idr:9:6:
|
9 | test : EvenList
| ^
When checking type of Main.test:
No such variable EvenList
reg006.idr:17:1-23:
|
17 | lookup k Leaf = Nothing
| ~~~~~~~~~~~~~~~~~~~~~~~
RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
reg007.lidr:8:3-13:
|
8 | > A.n = Z -- This is where it's at!
| ~~~~~~~~~~~
A.n is already defined
reg007.lidr:12:13-18:
|
12 | > hurrah = isSame
| ~~~~~~
When checking right hand side of hurrah with expected type
0 = 1
Type mismatch between
n = lala (Type of isSame)
and
0 = 1 (Expected type)
Specifically:
Type mismatch between
1
and
0
reg010.idr:5:3-26:
|
5 | unsafeSubst P x x px | _ = px
| ~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of with block in usubst.unsafeSubst:
Can't match on with block in usubst.unsafeSubst warg a P x x px
reg018a.idr:16:1-18:
|
16 | minusCoNat Z n = Z
| ~~~~~~~~~~~~~~~~~~
conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
reg018a.idr:21:1-42:
|
21 | loopForever = minusCoNat infinity infinity
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
conat.loopForever is possibly not total due to: conat.minusCoNat
reg018b.idr:8:1-28:
|
8 | showB (I x) = "I" ++ showB x
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A.showB is possibly not total due to recursive path A.showB --> A.showB
reg018b.idr:11:1-6:
|
11 | Show B where show = showB
| ~~~~~~
A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
reg018c.idr:21:1-22:21:
|
21 | inf (x :: xs) with (hdtl xs)
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
CodataTest.inf is possibly not total due to: with block in CodataTest.inf
reg018d.idr:8:1-39:
|
8 | pull {n=Z} _ (x :: xs) = (x, xs)
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.pull is not total as there are missing cases
reg023.idr:7:7:
|
7 | bad = Z
| ^
When checking right hand side of bad with expected type
f Nat
Type mismatch between
Nat (Type of 0)
and
f Nat (Expected type)
reg028.idr:5:1-9:
|
5 | bad Z = Z
| ~~~~~~~~~
tbad.bad is possibly not total due to: with block in tbad.bad
reg028a.idr:17:14-18:
|
17 | qsortLemma = proof
| ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.
reg028a.idr:11:1-14:
|
11 | qsort' [] = []
| ~~~~~~~~~~~~~~
tbad.qsort' is possibly not total due to: with block in tbad.qsort'
reg034.idr:6:1-14:
|
6 | bar xs xs Refl = Refl
| ~~~~~~~~~~~~~~
When checking left hand side of bar:
Can't match on bar xs xs Refl
reg034.idr:9:1-14:
|
9 | foo f x x Refl = Refl
| ~~~~~~~~~~~~~~
When checking left hand side of foo:
Can't match on foo f x x Refl
reg035b.idr:8:14-38:
|
8 | fins Z = ([] ** (finZEmpty {a=_}))
| ~~~~~~~~~~~~~~~~~~~~~~~~~
No such variable __pi_arg
reg044.idr:4:6-10:
|
4 | pf = proof
| ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.
reg044.idr:4:6-6:13:
|
4 | pf = proof
| ~~~~~ ...
When checking right hand side of Main.pf with expected type
(b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
Type mismatch between
b = b (Type of Refl)
and
a = b (Expected type)
Specifically:
Type mismatch between
b
and
a
reg049.idr:2:11-14:
|
2 | Bogus : Void
| ~~~~
When checking constructor Main.Bogus:
Void is not Main.Foo
reg049.idr:5:8-12:
|
5 | uhOh = Bogus
| ~~~~~
When checking right hand side of uhOh with expected type
Void
No such variable Bogus
badbangop.idr:7:1:
|
7 | (!) : List a -> Nat -> Maybe a
| ^
! is not a valid operator
baddoublebang.idr:6:28:
|
6 | doubleBang mmn = do pure !!mmn
| ^
unexpected Operator without known fixity: !!
reg054.idr:18:1-17:
|
18 | inf (MkInfer _ Z) = True
| ~~~~~~~~~~~~~~~~~
When checking left hand side of inf:
When checking an application of constructor Main.MkInfer:
Attempting concrete match on polymorphic argument: 0
reg054.idr:34:1-18:
|
34 | weird {x = Char} y = '5'
| ~~~~~~~~~~~~~~~~~~
When checking left hand side of weird:
No explicit types on left hand side: Char
reg054.idr:37:1-30:
|
37 | weird' {x = Prelude.Nat.Nat} y = Z
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of weird':
No explicit types on left hand side: Nat
reg054.idr:40:1-7:
|
40 | tctrick (Just x) = x
| ~~~~~~~
When checking left hand side of tctrick:
When checking an application of Main.tctrick:
Type mismatch between
Maybe a1 (Type of Just x)
and
a (Expected type)
reg055.idr:5:1-7:
|
5 | g (f Z) = 1
| ~~~~~~~
When checking left hand side of g:
Can't match on g (f 0)
reg055.idr:8:1-5:
|
8 | h x x = x
| ~~~~~
When checking left hand side of h:
Can't match on h x x
reg055a.idr:8:1-18:
|
8 | foo (CAny Nothing) = 42
| ~~~~~~~~~~~~~~~~~~
When checking left hand side of foo:
When checking an application of constructor Foo.CAny:
Attempting concrete match on polymorphic argument: Nothing
reg055a.idr:13:1-23:
|
13 | apply (\x => \y => x) a = a
| ~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of Foo.apply:
Can't match on apply (\x, y => x) a
reg056.idr:7:16-25:
|
7 | dodgy n m Refl impossible
| ~~~~~~~~~~
dodgy n m Refl is a valid case
reg056.idr:10:11-20:
|
10 | nonk Refl impossible
| ~~~~~~~~~~
nonk Refl is a valid case
reg068.idr:1:6-8:
|
1 | data nat : Type where --error
| ~~~
Main.nat has a name which may be implicitly bound.
This is likely to lead to problems!
reg068.idr:2:8-10:
|
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
| ~~~
Main.ze has a name which may be implicitly bound.
This is likely to lead to problems!
reg068.idr:2:8-10:
|
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
| ~~~
nat is bound as an implicit
Did you mean to refer to Main.nat?
reg068.idr:2:8-10:
|
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
| ~~~
When checking constructor Main.ze:
Type level variable nat is not Main.nat
Mod.idr:11:1-22:
|
11 | natexp k = S (natfn k)
| ~~~~~~~~~~~~~~~~~~~~~~
public export Mod.natexp can't refer to export Mod.natfn
reg070.idr:7:1-7:
|
7 | Show Te where
| ~~~~~~~
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
reg076.idr:8:1:
|
8 | <end of file>
| ^
Missing fixity declaration for Main.:>
reg077.idr:3:1:
|
3 | <end of file>
| ^
Missing fixity declaration for Main.:>>
DoubleEquality.idr:4:83-103:
|
4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
| ~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of oops with expected type
Void
When checking argument value to function Prelude.Basics.the:
Type mismatch between
x = x (Type of Refl)
and
(-0.0) = 0.0 (Expected type)
Specifically:
Type mismatch between
-0.0
and
0.0
Canonicity.idr:9:1-9:
|
9 | f Nil = 0
| ~~~~~~~~~
Canonicity.f is not total as there are missing cases
Canonicity.idr:12:1-20:
|
12 | NaN = f (Cons 0 Nil)
| ~~~~~~~~~~~~~~~~~~~~
Canonicity.NaN is possibly not total due to: Canonicity.f