andM package:Agda

andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
Agda Agda.Utils.Monad
type CommandM' = StateT CommandState
Agda Agda.Interaction.Base
type CommandM = CommandM' TCM
Agda Agda.Interaction.Command
localStateCommandM :: CommandM a -> CommandM a
Agda Agda.Interaction.Command
Restore both TCState and CommandState.
commandMToIO :: (forall x . () => (CommandM a -> IO x) -> IO x) -> CommandM a
Agda Agda.Interaction.InteractionTop
Opposite of liftIO for CommandM. This function should only be applied to computations that are guaranteed not to raise any errors (except for IOExceptions).
liftCommandMT :: (forall x . () => TCM x -> TCM x) -> CommandM a -> CommandM a
Agda Agda.Interaction.InteractionTop
Lift a TCM action transformer to a CommandM action transformer.
liftCommandMTLocalState :: (forall x . () => TCM x -> TCM x) -> CommandM a -> CommandM a
Agda Agda.Interaction.InteractionTop
Ditto, but restore state.
dropTypeAndModality :: LamBinding -> [LamBinding]
Agda Agda.Syntax.Concrete
Drop type annotations and lets from bindings.
namesAndMetasIn :: (NamesIn a, Collection QName m1, Collection MetaId m2) => a -> (m1, m2)
Agda Agda.Syntax.Internal.Names
Some or all of the names and meta-variables that can be found in the given thing.
namesAndMetasIn' :: (NamesIn a, Monoid m) => (Either QName MetaId -> m) -> a -> m
Agda Agda.Syntax.Internal.Names
Some or all of the names and meta-variables that can be found in the given thing.
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
Agda Agda.TypeChecking.MetaVars
Eta-expand a local meta-variable, if it is of the specified kind. Don't do anything if the meta-variable is a blocked term.
etaExpandMeta :: MonadMetaSolver m => [MetaClass] -> MetaId -> m ()
Agda Agda.TypeChecking.Monad.MetaVars
Eta-expand a local meta-variable, if it is of the specified class. Don't do anything if the meta-variable is a blocked term.
etaExpandMetaSafe :: MonadMetaSolver m => MetaId -> m ()
Agda Agda.TypeChecking.Monad.MetaVars
Do safe eta-expansions for meta (SingletonRecords,Levels).
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)]
Agda Agda.TypeChecking.Monad.MetaVars
Get all metas that correspond to unsolved interaction ids.
expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns
Agda Agda.TypeChecking.Rules.Term
Picks up record field assignments from modules that export a definition that has the same name as the missing field.