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