[−][src]Module agda_mode::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 |
| start_agda | Start the Agda process and return the stdio handles. |
Type Definitions
| AgdaResult | An Agda response that is either something good or some error. |
| NextResult | Return type of |