Typecheck a .ny file with a fresh Narya run (the authoritative check; slow: every import is loaded again).

Use it for the final verdict. While iterating on a file, keep a session instead: narya_start once, then edit the file and call narya_sync, which rechecks only the commands that changed. Returns ok (Narya accepted the file), clean (ok, with no assumed axioms and no open holes), errors with file/line/column, warnings, axioms assumed, holes, timing. Narya stops at the first error in a file. source_only=True ignores compiled .nyo files and rechecks every import from source (slow; for final checks). If loading compiled imports triggers a Narya anomaly, the file is rechecked from source automatically.

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.

Audit a file for unsound shortcuts: explicit axiom commands and holes in the file and its whole import closure (static scan following import/export statements), plus, if typecheck=True, a batch check reporting the axioms Narya actually assumed. verdict is "clean" only if nothing was found and the check passed.

Outline of a .ny file: its commands (def/axiom/notation/import/...) with names and line ranges, and which definitions contain holes. Static; does not run Narya.

Find declarations (lemmas, definitions, types) by name, words or meaning; Narya itself has no search command.

query may be words ("loop space of the circle"), identifiers or parts of them ("concat inverse"), a book label ("lem:circle-loopspace") or an exact name (ranked first). The index covers names, signatures, the comment above each declaration and the project's annotation files. With file (and optionally line), only declarations importable there are returned. With session_id and hole, the constants in the hole's type are added to the query and the scope is the session's file. kind: def, axiom, data, codata or record.

The full source of a declaration by exact name, with its location, comment and annotations (all files that define the name).

Start an interactive session (a live Narya process) and return its session_id and open holes.

With file: load the file command by command up to and including the command containing line (default: the whole file), stopping at the first error (error_at, messages). Holes created by the file are listed with their position in the file, context and type. With imports (module paths as in import "...", relative to directory or the file's directory): import them first; without a file this gives a scratch session for narya_exec / narya_synth. The first load of heavy imports can take a while; afterwards commands are fast. source_only=True loads imports from source instead of compiled files (slower; used automatically when loading compiled imports triggers a Narya anomaly).

Re-read the session's file after edits: retract the commands from the first changed one on (Narya undo) and replay the file up to and including the command containing line (default: the whole file). Unchanged commands, including all imports, are kept. Also moves the session backwards when line is earlier.

List the open holes of a session: number, position in the file (when known), context and type.

Run Narya commands in a session (def, axiom, echo, synth, notation, import, show, undo, ...), one after the other, stopping at the first failure. Returns each command's output, messages and new holes. Definitions made here are not in the file; narya_sync retracting past them undoes them too.

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.

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.

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.

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.

Close a session and stop its Narya process.

List live sessions (file, how far it is loaded, idle time, whether the file changed since).

Toolchain check: which project configuration applies (to file, or the default project), how Narya is run, its version, and the live sessions with their memory use where measurable.