Narya Synth
narya_synthSynthesize the type of a Narya term, optionally normalizing it, or infer types within a hole's context without committing changes.
Instructions
Synthesize the type of term (Narya synth), or with normalize=True also normalize it (Narya echo).
With hole, the term is elaborated in that hole's context (its variables are in scope). Nothing is committed.
Only synthesizing terms work (constants, applications, ascriptions (t : T)); a bare abstraction does not.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| hole | No | ||
| term | Yes | ||
| timeout | No | ||
| normalize | No | ||
| session_id | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||