Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Data type for all interactive responses



data DisplayInfo Source

Info to display at the end of an interactive command


Info_Constraints String 
Info_AllGoals String 
Info_Error String

When an error message is displayed this constructor should be used, if appropriate.

Info_Intro Doc

Info_Intro denotes two different types of errors TODO: split these into separate constructors

Info_Auto String

Info_Auto denotes either an error or a success (when Resp_GiveAction is present) TODO: split these into separate constructors

Info_ModuleContents Doc 
Info_NormalForm Doc 
Info_GoalType Doc 
Info_CurrentGoal Doc 
Info_InferredType Doc 
Info_Context Doc 


data Status Source

Status information.




sShowImplicitArguments :: Bool

Are implicit arguments displayed?

sChecked :: Bool

Has the module been successfully type checked?

data GiveResult Source

Give action result

Comment derived from agda2-mode.el

If GiveResult is 'Give_String s', then the goal is replaced by s, and otherwise the text inside the goal is retained (parenthesised if GiveResult is Give_Paren).

type InteractionOutputCallback = Response -> TCM ()Source

Callback fuction to call when there is a response to give to the interactive frontend.

Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.

Typical InteractionOutputCallback functions:

  • Convert the response into a String representation and print it on standard output (suitable for inter-process communication).
  • Put the response into a mutable variable stored in the closure of the InteractionOutputCallback function. (suitable for intra-process communication).

defaultInteractionOutputCallback :: InteractionOutputCallbackSource

The default InteractionOutputCallback function is set to __IMPOSSIBLE__ because in this way it is easier to recognize that some response is lost due to an uninitialized InteractionOutputCallback function.