[−][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? |