git.iko.soy/Idris-dev
on c7efd0a help sign in
Idris-dev/test/reg044/expected
13 lines 330 B history raw
1reg044.idr:4:6-11:
2This style of tactic proof is deprecated. See %runElab for the replacement.
3reg044.idr:4:4:When checking right hand side of Main.pf:
4Type mismatch between
5 b = b (Type of Refl)
6and
7 a = b (Expected type)
9Specifically:
10 Type mismatch between
11 b
12 and
13 a