[−][src]Module agda_mode::resp
Response data types (output of Agda).
Structs
| AgdaError | |
| AllGoalsWarnings | |
| AspectHighlight | A token highlighting information.
The token is somehow called |
| CmpSomething | |
| CommandState | |
| Context | |
| DefinitionSite | Jump to library definition information. |
| FindInstanceCandidate | |
| FindInstanceOF | |
| GiveAction | |
| GiveResult | Give action result |
| GoalSpecific | |
| GoalType | |
| Highlighting | A list of token highlighting information. |
| HighlightingInfo | |
| InferredType | |
| JustSomething | |
| MakeCase | |
| ModuleContents | |
| NamedPrettyTCM | |
| NormalForm | |
| OfType | |
| OneSolution | |
| OutputForm | |
| PostponedCheckArgs | |
| ResponseContextEntry | |
| Status | Status information. |
| TelescopicItem | One item in the |
| TypedAssign |
Enums
| DisplayInfo | Something that is displayed in the Emacs mode, serialized with more details. |
| GoalInfo | Information about one goal. |
| GoalTypeAux | |
| MakeCaseVariant | |
| OutputConstraint | |
| Resp | Agda response. |
Traits
| CollectObjs |
Type Definitions
| InvisibleGoal | |
| VisibleGoal |