Int package:Agda

Unfolding all metas before serialization.
An interactive computation.
File must exist.
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).
--interaction.
--interaction-json.