Narya Check
narya_checkTypecheck Narya command snippets against an existing file's imports and definitions using a reusable session, or validate standalone snippets with their own imports.
Instructions
Typecheck a snippet of Narya commands (defs, echo, synth, ...).
With file: in the context of that file (its imports and all its definitions), using a session for the file
(an open one is reused, otherwise one is started and kept, so later checks are fast); the snippet's definitions
are undone afterwards. This is the way to try out a lemma next to the code that needs it.
Without file: a fresh run in which the snippet must bring its own import "..." lines (relative to
directory); a snippet with holes fails, since open holes are an error at end of input.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file | No | ||
| source | Yes | ||
| timeout | No | ||
| directory | No |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||