Is a (WHNF) goal type in the cube or tope layer, so that a hole of this type is a cube point or a tope rather than a term? Used to suppress the type-layer-specific hole candidates (recOR, recBOT), which cannot inhabit a cube or a tope.

The names in scope a new one would shadow.

A fresh hole of the given type.

A hole carrying a name, so a suggested move can say what each of its holes stands for: id-hom ?A ?x rather than id-hom ? ?. The name is the Π binder's, so the move reads like the lemma's own signature, and two spines of the same lemma applied to different numbers of arguments are told apart by what the extra holes are called.

The constructors of a #data type former, in declaration order; empty for anything else. Found by their roles: the type former itself carries none, so the scan is over the names in scope.

The generated eliminators of a #data type former (ind-D before rec-D), with their roles.

A term of the given type built as λ-binders over a single typed hole (structurally: the motive types the generator builds are literal Π-chains). The eliminators pass such a motive so that their result type β-reduces to the hole and fits any goal, exactly like idJ's motive.

A match over a hypothesis, one branch per constructor with a hole body: the notational candidate offered beside the ind-/rec- spines. The node is display-only (its annotations are dropped before rendering), so its type infos are holes. Branch binders reuse the constructor's declared field names, with an induction hypothesis named ih, freshened against the names taken at the hole exactly as lambdaHoleOf freshens its motive binders.

Apply a term along its Π-type: a Just is the argument to use, a Nothing becomes a typed hole. Stops when the plan runs out.

How many branching eliminators allEliminationsInto will chain.

A forced Π-application is free (see allEliminationsInto), so this bounds only the Σ/cube projections and idJ steps, not the argument count of a spine. A temporary fixed bound: branching is shallow in the goals seen so far (a few projections), and a larger bound mostly adds self-referential spines (a built result eliminated again).

Whether eliminating a value spends the search budget. A forced Π-application is a SpineStep — there is one way to fill the argument (with a hole), so allEliminationsInto applies it for free; a Branching eliminator (a Σ/cube projection or idJ) costs one against maxEliminationDepth.

All ways to eliminate a hypothesis into a value usable at a goal.

Given a target type and a hypothesis term, return every elimination spine over that term whose type fits the target (or a subtype of it). Arguments introduced by application are left as holes for the caller to fill later. A value that already fits is returned as-is; a function is applied to holes; a Σ-type (or anything that unfolds to one, e.g. is-contr) is projected, possibly repeatedly — so first (first (is-segal-A ? ? ? ? ?)) is discovered.

A Π-application is a forced spine step, so it extends the spine for free and does not spend the budget. Only the genuinely branching eliminators count against maxEliminationDepth, so the bound limits real search depth, not argument count, and a lemma that must be applied to many holes is still reached.

A spine over a top-level hypothesis is emitted only once its meta prefix (see Rzk.TypeCheck.MetaPrefix) is fully applied: an unsaturated schema is not a suggestion, mirroring the warn-meta-prefix discipline. The search still passes through the unsaturated stages, so the saturated spines behind them are found; only the emission is gated.

Whether a term of the given (whnf) type may stand where a value of the target type is expected: the two types unify under structuralHoleUnify, so a hole acts as a wildcard leaf but a structural mismatch around it is still a mismatch (an under-applied function does not match an extension-type goal, but a partial application that genuinely fits an ordinary-function goal does).

The exception is a flexible type, one headed by a hole: it has no shape to mismatch with, so it fits any target. This is what makes an eliminator stated over a motive usable as a candidate --- ind-path ? ? ? ? ? ? has type ?C ?x ?p and so is offered at every goal, exactly as idJ already is, with the motive and the base case left as holes.

Outer type restrictions are stripped from both sides first: an extension-type boundary is satisfied by later refinement, not by the choice of spine, and matching against the restricted goal would reject the very spine that introduces the holes meant to satisfy it (f ? at a boundary goal, say).

Holes or constraints recorded while probing are discarded, so this is a pure yes/no query.

The eliminators a value of the given (weak head normal) type admits, each as a function wrapping the eliminated term, paired with its ElimCost.

A Π-type is eliminated by application to a fresh hole (a spine step); a Σ-type by either projection; an identity type by path induction (idJ), with the motive and base case left as holes. The projections and idJ branch. Anything else admits no simple eliminator.

The names taken at the hole (the source namespace) are passed in so that every binder an eliminator introduces (the idJ motive's \ b q → ?, a data eliminator's motive λs) is named in the move, freshened against them.

A scoped term that does not use its binder.

The motive \ b q → ? of a path induction: a type in the two motive binders, left as a hole.

The binder for a λ introduced over a domain type.

A binder the type already gives as a pattern is kept as-is — it carries the user's own names ((t , s)). Otherwise an explicit (pre-whnf) Σ-type or product domain is destructured into a fresh pair pattern, recursively for products, so that a nameless 2 × 2 × 2 parameter is introduced as ((t1 , t2) , t3) rather than a single opaque variable. Any other domain keeps its single binder.

Leaves are named by what they range over: a cube-product component is a point, named tN; a Σ component is a term, named xN. The names are display-only (the body is a hole that does not mention them) and carry a shared running index, so every leaf in the pattern is distinct.

All ways to introduce a value of a goal type by its head constructor, leaving the constituents as holes:

• a Π-type is introduced by a λ-abstraction over a hole body (\ x -> ?); the binder is taken from the type, so a pattern domain (a Δ² point (t , s), say) is introduced as \ (t , s) -> ?;
• a Σ-type or a cube product by a pair of holes ((? , ?));
• an identity type by refl, but only when its two endpoints already agree (otherwise refl would not typecheck);
• the unit type by unit;
• the tope universe by each tope constructor — TOP, BOT, ? ≡ ?, ? ≤ ?, ? ∧ ?, ? ∨ ? — so a shape (a hole of type TOPE) can be built up by tapping.

Unlike allEliminationsInto this does not search: a type has at most one introduction form (the tope universe is the one exception), read off its head constructor. Outer restrictions are stripped first, so an extension type is introduced by the form of its underlying type (its boundary is met by later refinement of the holes, not by the choice of constructor).

The λ binder of a Π-introduction is freshened against the names already visible at the hole, so introducing over a type whose own definition reuses an in-scope name (hom, whose internal binder is t) yields \ t₁ -> ? rather than a t that shadows the existing one.

Apply a term to holes through its whole Π-telescope: a datatype former applied through its parameters, so a U-goal offers coprod ? ?.

Whether the two endpoints of an identity type are definitionally equal, so that refl inhabits it. Like fitsInto, any holes or constraints recorded while probing are discarded, leaving a pure yes/no query.

Ex falso: in a contradictory tope context recBOT inhabits any type, so it is a candidate for every goal there (and only there — elsewhere it would not typecheck). Independent of the goal and of the local hypotheses.

Whether the local tope context is covered by the union of the given topes — the coverage obligation of recOR, as a yes/no query rather than a check that issues an error.

Tope case-split moves: ways to build a value of the goal by recOR, splitting the proof over a cover of the local tope context. Three sources, offered together (the UI ranks and filters):

• each disjunction ψ ∨ φ already in the context becomes recOR(ψ ↦ ?, φ ↦ ?) — its cover is immediate;
• when the goal is an extension type, its restriction faces are a cover candidate, offered only when they actually cover the context (so the move typechecks);
• a generic two-way split recOR(? ↦ ?, ? ↦ ?) with the guards left as holes, for an unusual split the player fills in by hand.

All three are offered only where a split makes sense — a cube variable is in scope, the context has a non-trivial tope, or the goal is a restricted type — so an ordinary (tope-free) goal is left alone.

The local hypotheses: everything in scope that is not a top-level entry.

The allow-listed top-level lemmas a hole's candidate list may draw on.

The elaboration environment at the current position: every in-scope entry contributes its source name — a pattern its leaves, as projection chains over the variable it binds — and an inner binding wins, exactly as the elaborator resolves an identifier written here. Kept as a table so sourceResolvesTo and parsesBackTo share it.

Does this variable's own source name, written at the current position, resolve back to it?

Does a rendered move, inserted as source text at the current position, parse and resolve back to the very term it renders? The comparison is α-equivalence of the untyped skeletons: a move is well-typed by construction, and insertion is a question of naming. This is the exact form of the old referability guard, and it enforces the move contract for everything emitted — a shadowing or unresolvable name anywhere in the rendering shows up as a resolution difference and drops the move.

Collapse a literal pair of matching projections, recursively along the pair spine: (π₁ p, π₂ p) reads back as p. This is exactly what the whole-point rendering of a pattern-bound variable parses to (the pattern (x, y) resolves to the projections), so the comparison in parsesBackTo absorbs the projection-folding convention.

Collapse a variable bound by the unit pattern to the constructor. A \ unit → … binds a point of Unit whose whole-point rendering (and the only way to write it) is unit, which parses back as the constructor. The two are the same point of the singleton, so the comparison in parsesBackTo treats them as one, exactly as pairEtaCollapse absorbs the projection-folding convention.

Record the goal and local context at a hole (lenient mode only).

Record a hole. When the hole is the argument of a shape-restricted function its goal is a shape: the cube goalTy together with a membership tope, which is a scope over the shape's bound variable. It is rendered under that binder, so the goal reads (binder : goalTy | tope).

Check a hole that appears as the argument of a shape-restricted function, whose domain is the cube cube restricted by tope (a scope over the domain's bound variable). Mirrors the hole case of typecheck, but records the shape as the hole's goal so the diagnostic shows (binder : cube | tope).

Check a recOR against a known expected type: each branch is checked against it under its own guard, the branches must agree on their overlaps, and together they must cover the context.

Drop the restriction faces of an extension type that are vacuous in the current tope context (their overlap with the context is the empty tope ⊥). A face mentioning an unfilled hole cannot be decided, so it is kept. Non-extension types are returned unchanged. Used when descending into a recOR branch, where the sibling branches' faces are disjoint from the branch guard.

How a match elaborates: which eliminator it targets, and — for ind-D — which variable scrutinee (if any) to abstract out of the goal when building the motive. Computed once from the into motive, the goal, and the scrutinee, so that the eliminator choice and the later motive construction read from the same decision instead of re-deriving it in two places.

Elaborate a match into an application of its datatype's induction eliminator: ind-D params motive method₁ … methodₖ indices scrutinee. The spine is the result — a match node never survives elaboration (see the ι-rule in Rzk.TypeCheck.Eval for how the spine then computes).

The motive is the elaborated into term when one was written; otherwise it is built from the goal, abstracting a variable scrutinee out of it (a non-variable scrutinee gives a constant family). Without into and without a goal (inference position) the match is rejected.

Check a branch's arm chain against its method type, one arm at a time, mirroring the λ rule: each arm's binder enters the context with the domain of the method's Π-type, and the elaborated arm becomes the method's λ under the same binder. Holes inside the branch body therefore see the branch binders as ordinary hypotheses, under the user's names.

β-reduce the administrative redexes elaboration introduces: a motive built as a λ-chain and applied to a constructor form is substituted through, so a branch hole's goal reads as the goal at that constructor (nat, or the substituted dependent goal) rather than as (λ x → …) (suc k). This is the labelled-goal restoration of the design: nothing else is unfolded — a motive that is a named family stays a named application.

The number of arms in a branch's chain (the binders the branch introduces).

The first name occurring twice, if any.

A motive built from the goal: λ-binders along the motive's Π-type (the family's indices, then the scrutinee), whose body is the goal — with the scrutinee variable replaced by the motive's own scrutinee binder, when the scrutinee is a variable. A non-variable scrutinee gives a constant family. (The motive types the eliminator generator builds are literal Π-chains, so matching them structurally is enough; cf. lambdaHoleOf.)

The type of the motive of a path induction: (z : A) → (a =_A z) → U.