Hoogle Search
Within LTS Haskell 24.25 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
-
Agda Agda.Compiler.Backend.Base Backend-specific top-level interactive command.
type
OldInteractionScopes = Map InteractionId ScopeInfoAgda Agda.Interaction.Base No documentation available.
oldInteractionScopes :: CommandState -> !OldInteractionScopesAgda Agda.Interaction.Base We remember (the scope of) old interaction points to make it possible to parse and compute highlighting information for the expression that it got replaced by.
theInteractionPoints :: CommandState -> [InteractionId]Agda Agda.Interaction.Base The interaction points of the buffer, in the order in which they appear in the buffer. The interaction points are recorded in theTCState, but when new interaction points are added by give or refine Agda does not ensure that the ranges of later interaction points are updated.
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]Agda Agda.Interaction.BasicOps getSolvedInteractionPoints True returns all solutions, even if just solved by another, non-interaction meta. getSolvedInteractionPoints False only returns metas that are solved by a non-meta.
runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()Agda Agda.Interaction.CommandLine No documentation available.
getOldInteractionScope :: InteractionId -> CommandM ScopeInfoAgda Agda.Interaction.InteractionTop No documentation available.
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()Agda Agda.Interaction.InteractionTop No documentation available.
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()Agda Agda.Interaction.InteractionTop A Lens for oldInteractionScopes.
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()Agda Agda.Interaction.InteractionTop A Lens for theInteractionPoints.