git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/test/reg044/expected
11 lines 235 B history raw
1reg044.idr:4:4:When checking right hand side of Main.pf:
2Type mismatch between
3 b = b (Type of Refl)
4and
5 a = b (Expected type)
7Specifically:
8 Type mismatch between
9 b
10 and
11 a