git.iko.soy/Idris-dev
on ca34dec help sign in
Idris-dev/test/error001/expected
13 lines 518 B history raw
1test002.idr:1:6:
2 |
31 | myid : (a : Type) -> a -> a
4 | ^
5Universe inconsistency.
6 Working on: ./test002.idr.z
7 Old domain: (6,6)
8 New domain: (6,5)
9 Involved constraints:
10 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
11 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
12 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}