| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Level.Solve
Synopsis
- defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a
- defaultLevelsToZero :: (PureTCM m, MonadMetaSolver m) => LocalMetaStore -> m ()
Documentation
defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a Source #
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.
defaultLevelsToZero :: (PureTCM m, MonadMetaSolver m) => LocalMetaStore -> m () Source #