Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant

Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.EmacsTop

Synopsis

mimicGHCi :: TCM () -> TCM ()
namedMetaOf :: OutputConstraint Expr a -> a
showGoals :: Goals -> TCM String
showInfoError :: Info_Error -> TCM String
explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc

Documentation

mimicGHCi :: TCM () -> TCM () Source #

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.

namedMetaOf :: OutputConstraint Expr a -> a Source #

showGoals :: Goals -> TCM String Source #

Print open metas nicely.

showInfoError :: Info_Error -> TCM String Source #

Serializing Info_Error

explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc Source #

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc Source #

Pretty-prints the type of the meta-variable.