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

Agda.TypeChecking.UniversePolymorphism

Documentation

mlevel :: MonadTCM tcm => tcm (Maybe Term)Source

compareLevel :: MonadTCM tcm => Comparison -> Term -> Term -> tcm Constraints Source

warshallConstraint :: Constraint -> TCM [Constraint]Source

solveLevelConstraints :: TCM ()Source