git.iko.soy/Idris-dev
on 8a3d348 help sign in
Idris-dev/test/error001/expected
9 lines 305 B history raw
1test002.idr:1:6:Universe inconsistency.
2Working on: z
3Old domain: Domain 6 6
4New domain: Domain 6 5
5Involved 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}