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