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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.EmacsTop

Synopsis

- mimicGHCi :: TCM () -> TCM ()
- namedMetaOf :: OutputConstraint Expr a -> a
- showGoals :: Goals -> TCM String
- showInfoError :: Info_Error -> TCM String
- explainWhyInScope :: MonadPretty m => WhyInScopeData -> m Doc
- prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM 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 :: MonadPretty m => WhyInScopeData -> m Doc Source #

prettyResponseContext Source #

Arguments

:: InteractionId | Context of this meta-variable.
-> Bool | Print the elements in reverse order?
-> [ResponseContextEntry] |
-> TCM Doc |

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

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

Pretty-prints the type of the meta-variable.