git.iko.soy/Idris-dev
on f0a67ff help sign in
Idris-dev/test/reg072/expected
15 lines 427 B history raw
1DoubleEquality.idr:4:87:
2When checking right hand side of oops with expected type
3 Void
5When checking argument value to function Prelude.Basics.the:
6 Type mismatch between
7 x = x (Type of Refl)
8 and
9 (-0.0) = 0.0 (Expected type)
11 Specifically:
12 Type mismatch between
13 -0.0
14 and
15 0.0