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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.LevelConstraints

Synopsis

Documentation

simplifyLevelConstraint :: Int -> Constraint -> Constraints -> Constraint Source #

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.