Agda.TypeChecking.LevelConstraints

Documentation

simplifyLevelConstraint :: Int -> Constraint -> Constraints -> Constraint

simplifyLevelConstraint n c cs turns an c into an equality constraint if it is an inequality constraint and the reverse inequality is contained in cs. Number n is the length of the context c is defined in.