Narya Search
narya_searchSearch Narya declarations by name, words, or meaning to find lemmas, definitions, and types. Filter by file, kind, or proof hole to locate importable results.
Instructions
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.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file | No | ||
| hole | No | ||
| kind | No | ||
| line | No | ||
| limit | No | ||
| query | No | ||
| session_id | No |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||