Narya Try
narya_tryCheck up to 20 candidate terms against a proof hole's type in context to see which typecheck, without solving it. Returns the first success and errors for others.
Instructions
Check up to 20 candidate terms against a hole's type, in its context, without solving it. Returns which candidates typecheck (with error messages for the others) and the first success. Commit with narya_solve.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| hole | Yes | ||
| terms | Yes | ||
| timeout | No | ||
| session_id | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||