Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.EmacsTop

Synopsis

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.

showGoals :: Goals -> TCM String Source #

Print open metas nicely.

showInfoError :: Info_Error -> TCM String Source #

Serializing Info_Error

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.