Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Level.Solve

Synopsis

Documentation

defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a Source #

Run the given action. At the end take all new metavariables of type level for which the only constraints are upper bounds on the level, and instantiate them to the lowest level.