| Safe Haskell | None |
|---|
Agda.TypeChecking.Reduce.Monad
- constructorForm :: Term -> ReduceM Term
- enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b
- underAbstraction_ :: Subst a => Abs a -> (a -> ReduceM b) -> ReduceM b
- getConstInfo :: HasConstInfo m => QName -> m Definition
- isInstantiatedMeta :: MetaId -> ReduceM Bool
- lookupMeta :: MetaId -> ReduceM MetaVariable
- reportSDoc :: VerboseKey -> Int -> TCM Doc -> ReduceM ()
- reportSLn :: VerboseKey -> Int -> String -> ReduceM ()
- traceSLn :: HasOptions m => VerboseKey -> Int -> String -> m a -> m a
- traceSDoc :: VerboseKey -> Int -> TCM Doc -> ReduceM a -> ReduceM a
Documentation
constructorForm :: Term -> ReduceM TermSource
enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM bSource
getConstInfo :: HasConstInfo m => QName -> m DefinitionSource
Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.
reportSDoc :: VerboseKey -> Int -> TCM Doc -> ReduceM ()Source
traceSLn :: HasOptions m => VerboseKey -> Int -> String -> m a -> m aSource