Agda.TypeChecking.Level.Solve

2 values

PackageAgda-2.8.0.2
Exports2
LanguageHaskell2010
LicenceMIT
SourceSolve.hs

valuedefaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a

Run the given action. If --cumulativity is off, that's it.

Otherwise, 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.

valuedefaultLevelsToZero

:: (PureTCM m, MonadMetaSolver m)
=> LocalMetaStore
-> m ()