[−][src]Module agda_mode::pos
Position types, used in both resp & cmd.
Structs
| InteractionPoint | |
| Interval | |
| Pos | A position in the file. |
Enums
| AgdaRange | IDK why is this needed, but Emacs passes it to Agda. It's fine to omit this in the commands. |
Type Definitions
| IntPos | |
| InteractionId | Normally, it's positive. |
| ProblemId | Normally, it's also positive. |