Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Reduce.Monad

Synopsis

Documentation

enterClosure :: LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b Source #

getConstInfo :: HasConstInfo m => QName -> m Definition Source #

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a Source #

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

Orphan instances