Narya Solve
narya_solveFill a proof hole with a term in its context, returning any new holes and the file edit to apply without modifying the file.
Instructions
Fill hole hole with term, checked in the hole's context (the term may contain new ? holes, which are
returned). This cannot be undone in Narya. The file is not modified: the result has an edit saying where
the hole is in the file; apply it, and keep the session in sync with narya_sync when you next need it.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| hole | Yes | ||
| term | Yes | ||
| timeout | No | ||
| session_id | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||