Look up a name and project one field of its VarInfo.

Is a surface name defined?

The free variables of a typed term, including those that occur only in the types of the variables it mentions.

A definition can depend on a section assumption without naming it: through the type of something else it uses. Closing a section has to see that dependency, and it is exactly what distinguishes an implicit assumption from an explicit one.

Instantiate a scoped term with an argument: the old substituteT.

The discreteness axiom a flat cube variable brings with it: a flat point of 2 (or of I) is one of the endpoints. Maintained at binder entry so that entailment does not have to rescan the context on every query.

What a binder adds to the context.

Run an action under a binder that has already been chosen.

Enter a fresh binder (one the checker invents) and run an action whose result says nothing about the new scope.

Open a scoped term under its own binder, run the action on the body, and pack the result back up as a scoped term.

Like underScope, for a Π (or a λ over a shape), which binds a tope scope beside the body under what the user wrote as one binder.

Open a scoped term for a computation whose result says nothing about the new scope (a check, or a rendered string).

Like inScope, for a binder that stands for a known value (a let).

Open a scoped term with a binder that has just been entered.

The scoped term lives in the enclosing scope, and so may be the codomain of the type a λ is being checked against, or the tope of a shape: all of them are opened under the one binder the λ introduces.

A scope that does not use its binder: the codomain of a non-dependent function type, say.

Enter the binder of an untyped scope — the body of a λ, or of a let, as the user wrote it — and elaborate it into a typed one.

The binder comes from the term being checked, and the scopes of the type it is checked against are opened under that same binder with openScoped.

Enter the binder of an untyped scope and run a computation under it.

The result may not mention the new scope — but a ScopedAST hides its scope, so the continuation can pack whatever it built with the binder it was given and hand back as many scoped terms as it likes. That is how a λ returns its elaborated body, its shape tope and the type it turned out to have, all at once.

Assume a tope for the enclosed action.

Install a deferred saturation cache for the transformed context, and run the action with it.

The pipeline's effects are discharged purely into a thunk: installing costs nothing, holes recorded by the speculative run are discarded, and a pipeline error (a tope guard with a hole in lenient mode, say, which the per-query path would never have evaluated) becomes Nothing, so errors surface exactly where they did before.

Run a check in every alternative of a disjunctive tope context.

Monadic all that stops at the first failing element.

The preprocessing entailM does before searching: dedup, split off the context's disjunctions, and saturate each alternative. Depends only on the given topes (plus the discreteness axioms of the context), not on the goal.

Search each saturated alternative for the goal.

Entailment against the context's own tope context, using the cached saturation when one was installed. Matching on the payload of SaturationCached is what forces the deferred pipeline, so the cost is paid at the first query under a context, and never for one that is never queried.

Ex falso for BOT, lifted across modalities.

A contradiction in the topes that are genuinely available at the identity modality entails BOT, and BOT entails _μ BOT for every modality μ by the absurd rule (this holds for BOT specifically; a general tope φ does NOT give _μ φ, which would need the missing unit id ⇒ μ). Re-asserting _μ BOT at each lock μ where an available tope was hidden lets the contradiction survive the lock: _b BOT is accessible under a _b lock (coe Flat Flat), so mod _b recBOT in a vacuous context is accepted.

A tope counts as available at the identity modality when its variable modality coerces into Id: a _b-modal tope qualifies via the counit (coe Flat Id), but a _#-modal one does not (coe Sharp Id is False) — which is exactly why _# BOT does not leak to plain BOT.

Is this cube point a lattice term (a sup or inf)? Used to keep the lattice-specific solver work (equality-to-order generation, the antisymmetry fallback for equality goals) off the equality-heavy non-lattice fragment, where it would only cost time without proving anything new.

Simplify the context, including disjunctions.

Accumulate a modality over a list of topes.

Is the local tope context contradictory (does it entail ⊥)?

Check that the local tope context is included in (entails) the union of the given topes. This is the COVERAGE obligation of recOR: every point of the context must be covered by some branch guard.

Only coverage is required, not equivalence: branch guards may overhang the context (when splitting with an already-defined shape, say), so we do not require OR(guards) |- context.

Diagnose a recOR branch guard or a restriction face against the local tope context. There are three cases, by how the tope relates to the context:

• DISJOINT — the tope and a consistent context have empty overlap (their conjunction is ⊥). The face or branch is then vacuous everywhere, so this is a hard error.
• OVERHANG — the tope is not entailed by the context but still overlaps it. This is allowed and often intentional (splitting or restricting with an already-defined shape, whose faces live on the whole cube rather than being relativised to the context), so we only emit a non-fatal hint.
• CONTAINED — the tope entails the context: nothing to report.

The term a restriction face pins down, when one of the faces holds.

Perform at most one η-expansion at the top level, to assist unification.

Memoise a term's WHNF on its top node without reducing the term itself.

The returned term has the same (unreduced) structure, so free-variable and uses detection see exactly what the user wrote, while a later whnfT is O(1) via the cached form. Used when storing a definition's elaborated type and value, where an in-place reduction could otherwise discard or expose a variable occurrence.

The branch of a recOR (or the face of a restriction) whose guard holds.

The head of an application spine and its arguments, in application order, each paired with the type annotation of its AppT node (needed to rebuild a neutral application).

Apply a function term to a spine of arguments, reducing.

Try to fire a #data ι-rule on an application spine: the head is a generated eliminator, the scrutinee argument is headed by a fully applied constructor of the same datatype. Returns the method applied to the constructor's fields (and any leftover spine arguments), unreduced.

A non-Var head answers Nothing immediately, so the common neutral spine pays one pattern match; a Var head pays one lookupVarInfo.

Apply a term to arguments left to right, annotating each application node with its actual type. The spine machinery reuses the annotations of existing nodes, which a freshly built ι-redex does not have.

Peel the head's syntactic lambda chain into one substitution, then reduce. subst maps the binders consumed so far to their arguments; body is the current lambda's body, at the scope those binders extended into.

Apply a non-lambda (already WHNF) function to a spine, one argument at a time: this is the type-directed part of application, unchanged from before.

Apply a non-lambda function f' (already WHNF) to one argument x. A shape-restricted function contributes a tope side-condition; a function whose return type is restricted refines the application's type; everything else is a neutral application. Extracted verbatim from the old single-argument AppT case.