agda_retrieve_context
Retrieve the type and local context associated with an Agda goal handle, enabling inspection of the current proof state and informed next steps.
Instructions
Retrieve the type and local context for an opaque goal handle
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| goal | Yes | Opaque goal handle returned by the latest module state | |
| async | No | true always returns a job handle; false blocks until Agda finishes | |
| rewrite | No | ||
| timeoutMs | No | Override the configured Agda command timeout for this call | |
| includeRaw | No | Include Agda's native event log; omitted by default because it is large | |
| deferAfterMs | No | How long this call may block before returning a job handle; capped by maxJobWaitMs |