agda_retrieve_constraints
Retrieve type constraints from the active Agda module in a workspace to inspect unsolved metas and outstanding proof obligations.
Instructions
Retrieve constraints for the active module in a workspace
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 |