HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Level.Solve

  • 2 values
  • PackageAgda-2.7.0.1
  • Exports2
  • LanguageHaskell2010
  • LicenceMIT
  • SourceSolve.hs
valuedefaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a
#

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.