[−][src]Module agda_mode::cmd
Agda commands (input to Agda).
Structs
| GoalInput | Text in the goal. |
| IOTCM | |
| InputWithRewrite |
Enums
| Cmd | |
| HighlightingLevel | How much highlighting should be sent to the user interface? |
| HighlightingMethod | How should highlighting be sent to the user interface? |