Agda-2.2.10: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.UniversePolymorphism
mlevel :: MonadTCM tcm => tcm (Maybe Term)Source
compareLevel :: MonadTCM tcm => Comparison -> Term -> Term -> tcm ConstraintsSource
warshallConstraint :: Constraint -> TCM [Constraint]Source
solveLevelConstraints :: TCM ()Source