@@ -7,8 +7,7 @@ No such variable EvenList
77reg006.idr:17:1:
88RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
99reg007.lidr:8:1:A.n is already defined
10−reg007.lidr:12:11-17:
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
1211 0 = 1
1312
1413Type mismatch between
@@ -54,8 +53,7 @@ Can't match on foo f x x Refl
5453reg035b.idr:8:6:No such variable __pi_arg
5554reg044.idr:4:6-11:
5655This style of tactic proof is deprecated. See %runElab for the replacement.
57−reg044.idr:4:4:
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
5957 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
6058
6159Type mismatch between
@@ -70,8 +68,7 @@ Specifically:
7068 a
7169reg049.idr:2:9:When checking constructor Main.Bogus:
7270Void is not Main.Foo
73−reg049.idr:5:6:
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
7572 Void
7673
7774No such variable Bogus
@@ -109,8 +106,7 @@ reg055a.idr:13:7:When checking left hand side of Foo.apply:
109106Can't match on apply (\x => \y => x) a
110107reg056.idr:7:7:dodgy n m Refl is a valid case
111108reg056.idr:10:6:nonk Refl is a valid case
112−reg068.idr:1:6:
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.
114110This is likely to lead to problems!
115111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
116112This is likely to lead to problems!
@@ -118,12 +114,10 @@ reg068.idr:2:8-11:WARNING: nat is bound as an implicit
118114 Did you mean to refer to Main.nat?
119115reg068.idr:2:6:When checking constructor Main.ze:
120116Type level variable nat is not Main.nat
121−Mod.idr:11:1:
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
123118reg070.idr:7:1:
124119Test_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
127121 Void
128122
129123When checking argument value to function Prelude.Basics.the: