Expand description
Response data types (output of Agda).
Structs§
- Agda
Error - AllGoals
Warnings - Aspect
Highlight - A token highlighting information.
The token is somehow called
Aspectin Agda. - CmpSomething
- Command
State - Context
- Definition
Site - Jump to library definition information.
- Find
Instance Candidate - Find
InstanceOF - Give
Action - Give
Result - Give action result
- Goal
Specific - Goal
Type - Highlighting
- A list of token highlighting information.
- Highlighting
Info - Inferred
Type - Just
Something - Make
Case - Module
Contents - Named
PrettyTCM - Normal
Form - OfType
- OneSolution
- Output
Form - Postponed
Check Args - Response
Context Entry - Status
- Status information.
- Telescopic
Item - One item in the
telToListtelescope list. - Typed
Assign
Enums§
- Display
Info - Something that is displayed in the Emacs mode, serialized with more details.
- Goal
Info - Information about one goal.
- Goal
Type Aux - Make
Case Variant - Output
Constraint - Resp
- Agda response.