ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.EmacsTop

Synopsis

valuemimicGHCi :: TCM () -> TCM ()

mimicGHCi is a fake ghci interpreter for the Emacs frontend and for interaction tests.

mimicGHCi reads the Emacs frontend commands from stdin, interprets them and print the result into stdout.

valuenamedMetaOf :: OutputConstraint Expr a -> a

valueshowGoals :: Goals -> TCM String

Print open metas nicely.

valueshowInfoError :: Info_Error -> TCM String

Serializing Info_Error

valueexplainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc

valueprettyResponseContext

Pretty-prints the context of the given meta-variable.

valueprettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc

Pretty-prints the type of the meta-variable.