Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.LevelConstraints

Synopsis

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

# 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.