git.iko.soy/Idris-dev
on bd8ea0a help sign in
Idris-dev/test/error001/expected
8 lines 469 B history raw
1test002.idr:1:6:Universe inconsistency.
2 Working on: ./test002.idr.z
3 Old domain: (6,6)
4 New domain: (6,5)
5 Involved constraints:
6 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
7 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
8 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}