Narya Split
narya_splitPreview a proof hole's solution shape without committing it: split on the goal type or, given datatype terms, into one branch per constructor.
Instructions
Ask Narya for the shape of a solution of a hole without committing it. Without term: split on the goal
type (abstraction for a function type, tuple for a record, comatch for codata, constructor for a one-constructor
datatype). With term (or comma-separated terms) of a datatype: a match with one branch per constructor.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| hole | Yes | ||
| term | No | ||
| timeout | No | ||
| session_id | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||