idris-1.2.0: test/totality014/expected
totality014.idr:1:6-9:
|
1 | data Con2 : Type where
| ~~~~
Universe inconsistency.
Working on: ./totality014.idr.w
Old domain: (5,5)
New domain: (5,4)
Involved constraints:
ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:29}