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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Reduce.Monad

Synopsis

Documentation

enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b Source

underAbstraction_ :: Subst t a => Abs a -> (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.

traceSLn :: HasOptions m => VerboseKey -> Int -> String -> m a -> m a Source

applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (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.