@@ -7,8 +7,7 @@ No such variable EvenList
7reg006.idr:17:1:
7reg006.idr:17:1:
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
9reg007.lidr:8:1:A.n is already defined
9reg007.lidr:8:1:A.n is already defined
11−When checking right hand side of hurrah with expected type
10+reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type
14Type mismatch between
13Type mismatch between
@@ -54,8 +53,7 @@ Can't match on foo f x x Refl
54reg035b.idr:8:6:No such variable __pi_arg
53reg035b.idr:8:6:No such variable __pi_arg
55reg044.idr:4:6-11:
54reg044.idr:4:6-11:
56This style of tactic proof is deprecated. See %runElab for the replacement.
55This style of tactic proof is deprecated. See %runElab for the replacement.
58−When checking right hand side of Main.pf with expected type
56+reg044.idr:4:4:When checking right hand side of Main.pf with expected type
59 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
57 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
61Type mismatch between
59Type mismatch between
@@ -70,8 +68,7 @@ Specifically:
71reg049.idr:2:9:When checking constructor Main.Bogus:
69reg049.idr:2:9:When checking constructor Main.Bogus:
72Void is not Main.Foo
70Void is not Main.Foo
74−When checking right hand side of uhOh with expected type
71+reg049.idr:5:6:When checking right hand side of uhOh with expected type
77No such variable Bogus
74No such variable Bogus
@@ -109,8 +106,7 @@ reg055a.idr:13:7:When checking left hand side of Foo.apply:
109Can't match on apply (\x => \y => x) a
106Can't match on apply (\x => \y => x) a
110reg056.idr:7:7:dodgy n m Refl is a valid case
107reg056.idr:7:7:dodgy n m Refl is a valid case
111reg056.idr:10:6:nonk Refl is a valid case
108reg056.idr:10:6:nonk Refl is a valid case
113−Main.nat has a name which may be implicitly bound.
109+reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
114This is likely to lead to problems!
110This is likely to lead to problems!
115reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
116This is likely to lead to problems!
112This is likely to lead to problems!
@@ -118,12 +114,10 @@ reg068.idr:2:8-11:WARNING: nat is bound as an implicit
118 Did you mean to refer to Main.nat?
114 Did you mean to refer to Main.nat?
119reg068.idr:2:6:When checking constructor Main.ze:
115reg068.idr:2:6:When checking constructor Main.ze:
120Type level variable nat is not Main.nat
116Type level variable nat is not Main.nat
122−public export Mod.natexp can't refer to export Mod.natfn
117+Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn
123reg070.idr:7:1:
118reg070.idr:7:1:
124Test_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
119Test_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
125−DoubleEquality.idr:4:87:
126−When checking right hand side of oops with expected type
120+DoubleEquality.idr:4:87:When checking right hand side of oops with expected type
129When checking argument value to function Prelude.Basics.the:
123When checking argument value to function Prelude.Basics.the: