Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- constructorForm :: HasBuiltins m => Term -> m Term
- enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b
- underAbstraction :: (MonadReduce m, Subst t a) => Dom Type -> Abs a -> (a -> m b) -> m b
- underAbstraction_ :: (MonadReduce m, Subst t a) => Abs a -> (a -> m b) -> m b
- addCtxTel :: MonadReduce m => Telescope -> m a -> m a
- getConstInfo :: HasConstInfo m => QName -> m Definition
- isInstantiatedMeta :: MetaId -> ReduceM Bool
- lookupMeta :: MetaId -> ReduceM MetaVariable
- askR :: ReduceM ReduceEnv
- applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (m a -> m a) -> m a -> m a
Documentation
constructorForm :: HasBuiltins m => Term -> m Term Source #
underAbstraction :: (MonadReduce m, Subst t a) => Dom Type -> Abs a -> (a -> m b) -> m b Source #
underAbstraction_ :: (MonadReduce m, Subst t a) => Abs a -> (a -> m b) -> m b Source #
addCtxTel :: MonadReduce m => Telescope -> m a -> m a 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.
lookupMeta :: MetaId -> ReduceM MetaVariable 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.