git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/totality014/expected
8 lines 510 B history raw
1totality014.idr:1:6:Universe inconsistency.
2 Working on: ./totality014.idr.w
3 Old domain: (5,5)
4 New domain: (5,4)
5 Involved constraints:
6 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}
7 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}
8 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}