Sinking a whole list is a coercion too, with no per-element rebuild.

The per-file groups also sink by coercion. sink1 cannot see through the pair (its element must be the sunk type itself), but the sinkability argument is the same: only the declarations mention the scope.

What a run of the checker produced: the top-level scope, the declarations in it, and the errors found.

The scope is existential, and the declarations live in it. Anything that wants to resume from a checked prefix (the LSP's incremental path) keeps the whole package and carries on from that context; anything that only displays them reads them through the context's naming.

Bind a top-level entry and run the rest of the module under it.

Record a new entry in the innermost open section.

Close a section: abstract each of its assumptions out of the definitions that used it, report the ones that went unused, and take the assumptions back out of scope.

The definitions stay in scope, with their entries rewritten to take the assumption as an explicit parameter. The assumptions' names stay in the /scope index/ — a scope only ever grows — but they are removed from the surface-name map and from the list of what is in scope, so they can no longer be referred to, shown, or shadowed.

An error, captured in the current context (rather than thrown).

Turn the section's entries into declarations, abstracting each assumption out of the definitions that follow it.

The entries come newest first, so the definitions accumulated in recent are exactly those that could have used the assumption currently being processed.

Abstract one assumption out of the definitions that come after it.

A definition that mentions the assumption gains it as an explicit parameter, and every later definition that mentions that definition is rewritten to apply it to the assumption. A definition that mentions it without declaring it in its uses clause is an implicit assumption, and an error. | Whether an assumption was taken up by (abstracted into) any definition that followed it in its section.

Give an entry the assumption as an explicit parameter.

Rewrite every use of a definition into an application of it to the assumption it has just been abstracted over.

The index telescope of the sort. The sort must be U (no indices) or a Π-telescope of plain types ending in U.

The parameters of a #data must be plain typed variables (x : A): the constructors and eliminators apply the type former to them.

A constructor field: a typed parameter, with cube/shape fields rejected (over a directed interval they would declare directed cells, out of scope for M3) and modal fields deferred (crisp induction).

The assumptions an entry depends on, possibly only through the types of what it mentions. The generated entries of a #data declare these dependencies, so that closing a section abstracts the assumption over all of them uniformly instead of reporting an implicit assumption.

Several distinct fresh identifiers with a shared base.

An identifier that is neither bound at the top level nor among the given local binder tokens; primes are appended until one is free. Used for the motive and scrutinee binders of the generated eliminator types, which close over the user's field types.

Bind the products of one #data declaration: the type former, the constructors (checked in a scope where the type former exists), and the generated eliminators ind-D and rec-D.

Run a command, recording which one it is and where.

An error raised anywhere in the command (or in the rest of the module, which is checked inside it) is collected rather than thrown: the declarations made before it stand, the error is reported, and the rest of the module is skipped. The strict entry points turn the first collected error back into a thrown one.

The binder leaves repeated within one binder group of a surface command: the parameter list of a λ, of a declaration, or of a constructor (a single pattern's leaves are part of their group). Each hit pairs the repeated occurrence with the earlier ones it clashes with.

Shadowing an outer binder stays a warning (checkNameShadowing); a duplicate inside one group can only be a mistake, and the silent freshening it used to get showed names the user never wrote (issue #321).

Report a command's error and go on to the next one, with the command itself contributing nothing to the scope.

This is the recovery for a command that cannot be stood in for: a declaration whose type does not check has no type to enter it at. The uses of it below then report an undefined variable, which is noisier than the one error but keeps the rest of the file's own errors and holes visible, which is what a file being edited is wanted for.

Run a check, handing back its error instead of propagating it.

What it recorded on the way is kept: the record lives in the state beneath the error channel, so the holes the user wrote in a definition that fails are still reported (see Rzk.TypeCheck.Monad).

Run a check with the location narrowed to where a surface term was written.

Descending through a judgement already narrows to the sub-term it is about (narrowLocation in Rzk.TypeCheck.Monad), but only a node carries a position: a variable is a leaf of the core syntax, with nowhere to put one. So a check that starts from a surface term says where that term starts, and a definition whose body is a bare variable is reported at the body rather than at the declaration above it.

Elaborate a surface term in the current top-level scope: a free identifier resolves to the top-level entry it names.

Is a surface identifier defined at the top level?

Check a module's commands, extending the scope with each definition.

The continuation runs in the final scope, with the declarations the module produced (sunk into it) and the errors found.

Assume a list of names of the same type, each a top-level entry.

Check the commands of a section, then close it.

Check one module.

Check a list of modules, one after another, in a scope that grows as it goes.

Checking stops at the first module with an error, as it did before.

Check the modules, and package the result with the scope it was checked in. The warnings are recorded during the run and are folded into the Checked package here.

Check the modules strictly: an unfilled hole is an error, and the first error stops the run.

Check the modules in lenient hole mode, returning the holes recorded (each with its goal and local context). This is the structured goal/context query the LSP and the game consume.

Like typecheckModulesWithHoles, but additionally offers the given named top-level definitions as hole candidates (each applied to holes when its type fits the goal, and never below its meta prefix — an unsaturated schema is not a suggestion, see Rzk.TypeCheck.MetaPrefix). The game passes a level's allow-list of relevant lemmas so they surface as moves; an empty list reproduces typecheckModulesWithHoles.

A declaration, rendered: no scope index, and nothing to re-elaborate.

This is what the LSP shows — a name, a type, a location — and it is all it needs. The elaborated terms stay inside the Checked package, which is what a resume needs.

What kind of declaration a DeclView renders: a plain definition, a postulate, or one of the products of a #data (the symbol providers group constructors under their type and keep the generated eliminators out of the outline; the semantic tokens highlight postulates distinctly).

The declarations of a checked run, rendered, grouped by the file they came from.

Continue checking from a prefix that has already been checked.

This is the incremental path: the cached context is the elaborated prefix, so nothing is replayed and nothing is re-elaborated.

The errors of a checked run.

The warnings of a checked run.

Nothing checked yet: the empty context, and no declarations.

Nothing checked yet, in lenient hole mode: what an editor resumes from.

A hole is work in progress there, to be reported with its goal and context rather than as an error (see allowHoles). recheckFrom continues in the context it is given, so the mode has to be set on the empty one it starts with: resuming from emptyChecked made every hole a TypeErrorUnsolvedHole and stopped the file at the first one.