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

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 #