Module agda 

Invoke Agda in command line and interact with it via stdio.

Modules

verify

Verify whether Agda is working.

Structs

AgdaRead

JustStdio

ProcessStdio

ReplState

Simple REPL state wrapper.

Constants

INTERACTION_COMMAND

START_FAIL

Functions

deserialize_agda

Deserialize from Agda’s command line output.

init_agda_process

load_file

Common command: load file in Agda.

preprint_agda_result

send_command

Send an IOTCM command to Agda.

start_agda

Start the Agda process and return the stdio handles.

Type Aliases

AgdaResult

An Agda response that is either something good or some error.

NextResult

Return type of next_* functions.