idris-0.12.3: test/basic018/expected
basic018.idr:7:12-17:WARNING: thing is bound as an implicit
Did you mean to refer to Main.thing?
basic018.idr:12:8-13:WARNING: thing is bound as an implicit
Did you mean to refer to Main.thing?
basic018.idr:13:6:When checking right hand side of test with expected type
thing = S 41
Type mismatch between
42 = 42 (Type of Refl)
and
thing = 42 (Expected type)
Specifically:
Type mismatch between
42
and
thing