agda_retrieve_goals
Retrieve the current visible goals and opaque handles from an Agda module workspace, enabling inspection of proof obligations.
Instructions
Retrieve the current visible goals and opaque handles
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| async | No | true always returns a job handle; false blocks until Agda finishes | |
| timeoutMs | No | Override the configured Agda command timeout for this call | |
| workspace | Yes | Opaque workspace handle returned by agda_load_module | |
| 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 |