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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Level.Solve

Synopsis

- defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a
- defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => MetaStore -> m ()

# 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.

defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => MetaStore -> m () Source #