[−][src]Module agda_mode::resp
Response data types (output of Agda).
Structs
| AspectHighlight | |
| CommandState | |
| DefinitionSite | |
| HighlightingInfo | |
| ResponseContextEntry | |
| Status |
Enums
| DisplayInfo | |
| GoalInfo | |
| GoalTypeAux | |
| MakeCase | |
| Resp | TODO: This enum is incomplete, contribution is welcomed. |