Workspace-wide symbol search over every typechecked module in the cache. The query is matched case-insensitively as an infix of the definition name; an empty query lists all definitions (clients filter further as the user types).

A signature for the hover code block. A long function type is split with one parameter per line, in the style rzk definitions are written:

is-equiv
  : ( A : U)
  → ( B : U)
  → ( f : A → B)
  → U

The checker-derived token overlay for identifier uses: an occurrence that resolves to a product of a #data declaration is coloured by its kind wherever it appears — a constructor as an enum member, the type as a class, a generated eliminator as a library function — and an occurrence of a postulate or an assumption is marked abstract (declared, but not proven), so a proof that leans on an axiom is visible at a glance. Postulates, top-level assumptions, and in-section assumptions get distinct type/modifier combinations, in decreasing order of severity. Occurrences are matched to declarations by definition site (file and line) and name, so a local that shadows a constructor stays plain, and plain definitions are left to the lexer baseline. Positions are code points, like every other token source; the UTF-16 conversion happens after merging.

The cache eviction and the re-typecheck run on the typecheck worker thread, so this handler returns immediately and later requests (e.g. a formatting request from format-on-save) are answered while the project re-check is still running. Spawning the worker cancels the previous one, so a newer change restarts the re-check.