Like defaultTypeCheck, but runs in lenient hole mode (allowHoles) and also returns the holes recorded during checking (with their goal and context).

Typecheck modules in lenient hole mode, returning the elaborated declarations, any type errors, and the holes recorded (each with its goal and local context). This is the structured goal/context query consumed by the LSP and the game. Strict callers (the default CLI path, CI) keep using typecheckModulesWithLocation, where holes are TypeErrorUnsolvedHole.

Like typecheckModulesWithHoles, but additionally offers the given named top-level definitions as hole candidates (each applied to holes when its type fits the goal). The game passes a level's allow-list of relevant lemmas so they surface as moves; an empty list reproduces typecheckModulesWithHoles.

Render a type error, folding pattern-binder projections (e.g. π₁ x back to the user's t) and showing a bare pattern point as the pattern, using the context's freshened binders (see contextBinders).

The pattern binders in scope, freshened and keyed by their (current) name, together with the projection-folding map derived from them. Both share the same freshened component names, so a term's projections and the binder shown in the context agree.

Render an (untyped) term for an error or diagnostic message, given the context's freshened pattern binders: fold a pattern-binder variable's projections to their component names, then expand a bare use of the variable to the pattern itself (see foldBinderProjections and restorePatternVars). An empty binder list renders the term as-is.

Like ppFoldU for a type-annotated term, shown as term : type with the same folding and pattern restoration applied to both halves.

Freshen the compound (pattern) binders in scope so their component names avoid the display names already in use and one another. Returns each relevant variable paired with its freshened binder. Variables bound to a single name are omitted: they need no projection folding and are displayed normally.

The projection-folding map for rendering: each pattern-binder variable's display name mapped to the projection paths of its component names (e.g. π₁ ↦ t, π₂ ↦ s). Ordinary projections (of non-pattern variables) are left untouched.

Classify a (WHNF) type as a cube, so cube variables (e.g. t : 2) are shown separately from ordinary term variables in a hole's context.

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

Is this term a hole? Holes only exist in lenient mode (see allowHoles); they are opaque placeholders standing for a term of the expected type.

Does this term contain a hole anywhere (including nested, e.g. f ?)? Used to keep unification lenient around incomplete terms: a term with an unfilled hole cannot be meaningfully compared, so a unification that would otherwise fail is deferred. Evaluated only on the failure path.

All ways to eliminate a hypothesis into a value usable at a goal. Given a target type and a hypothesis term (e.g. Pure v for a context variable), 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 e.g. first (first (is-segal-A ? ? ? ? ?)) is discovered.

The search is driven uniformly by the eliminators a (weak head normal) type admits (see eliminatorsOf), so adding a new eliminator extends it without touching the search.

A Π-application is a forced spine step — there is exactly one way to fill an argument (with a hole) — so it extends the spine for free and does not spend the budget. Only the genuinely branching eliminators (Σ/cube projections and idJ, flagged by eliminatorsOf) count against maxEliminationDepth. The bound therefore limits real search depth, not argument count, so a lemma that must be applied to many holes is still reached. The free spine terminates because each application strips one Π binder off a finite type.

How many branching eliminators allEliminationsInto will chain. Forced Π-applications are 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). It should be made configurable once there is more evidence of what real goals need.

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).

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 (e.g. f ? at a boundary goal).

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

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.

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 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 (e.g. (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 t/s-style as 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. Given a target type, return its introduction forms:

• a Π-type is introduced by a λ-abstraction over a hole body (\ x -> ?); the binder is taken from the type, so a pattern domain (e.g. a Δ² point (t , s)) 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.

Any other type admits no simple introduction. Unlike allEliminationsInto this does not search: a type has at most one introduction form (the tope universe is the one exception), read off its (weak head normal) head constructor. Outer type 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 inScope (the names already visible at the hole), so introducing over a type whose own definition reuses an in-scope name (e.g. hom, whose internal binder is t) yields \ t₁ -> ? rather than a t that shadows the existing one.

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.

Whether the local tope context is contradictory (entails ⊥). Reads the precomputed flag when present, falling back to an entailment check. Used to decide whether recBOT (ex falso) is available.

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 (see contextEntailsUnion), but as a pure 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 recOR(ψ₁ ↦ ?, …), 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 in a setting 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.

Record the goal and local context at a hole (lenient mode only). The goal, the local hypotheses, and the tope assumptions are all rendered to user-facing VarIdent names here — reusing the same resolution as ppTermInContext — so the resulting HoleInfo is independent of the De Bruijn scope. The global environment is deliberately excluded (only varIsTopLevel == False locals are kept), and locals are split into cube variables and ordinary term variables.

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. The tope is a scope over the shape's bound variable (the third argument carries the declared binder name, if any, and the tope); 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).

Run the enclosed action with the renderHideTerm policy set.

Render the enclosed action with the proof term hidden (see renderHideTerm).

Switch to lenient hole mode: record each hole's goal and context instead of reporting it as an error. Used by the structured goal/context query and the --allow-holes CLI mode; the default (strict) mode rejects holes.

Allow a hole's candidate list to draw on the given named top-level definitions (in addition to the local hypotheses). The game supplies the per-level allow-list; recordHoleShape then offers each listed lemma whose type fits the goal, applied to holes. See hintLemmas.

Within the given action, a hole unifies only as a leaf in an otherwise matching structure: a structural mismatch around a hole stays an error rather than being deferred (see deferHoleMismatches). Used to ask whether a term could have a given type, as opposed to tolerating an in-progress sketch.

The full binder (pattern) of each in-scope variable, used to restore pattern-binder component names (e.g. t/s for \ (t , s) -> …) when rendering goals, holes and contexts.

A binding shown in a hole's local context: the display name and its type, already rendered with user-facing VarIdent names (see HoleInfo).

The structured goal and context at a hole, recorded in lenient mode (see allowHoles). Everything is rendered to user-facing VarIdent names at record time, so HoleInfo is independent of the De Bruijn scope it came from. Local hypotheses are split into ordinary term variables and cube variables (the cube/tope layer is specific to Rzk); the global environment is deliberately excluded — it belongs in a searchable inventory, not the goal panel.

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: e.g. _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 (see ill-modal-sharp-bot-not-bot).

Simplify the context, including disjunctions. See also simplifyLHS.

Simplify the context, except disjunctions. See also simplifyLHSwithDisjunctions.

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.

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

Diagnose a recOR branch guard or 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/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 (e.g. 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. The hint is gated at Normal verbosity, hence silent under Silent (e.g. in tests).
• CONTAINED — the tope entails the context: nothing to report.

Run a sub-scope computation and lift it back to the enclosing scope: close the error channel one binder with ScopedTypeError (as before), and re-emit the holes it recorded. HoleInfo is already rendered to VarIdent names, so no De Bruijn re-indexing is needed — only a plain re-tell. On a thrown error the sub-scope's holes are dropped, which is intended: holes only matter on the success path (lenient mode), and strict mode wants the error anyway.

Perform at most one \(\eta\)-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 infoWHNF. Used when storing a definition's elaborated type and value, where an in-place reduction could otherwise discard or expose a variable occurrence.

Compute a typed term to its WHNF.

>>> unsafeTypeCheck' $ whnfT "(\\ (x : Unit) -> x) unit"
unit : Unit

Compute a typed term to its NF.

>>> unsafeTypeCheck' $ nfT "(\\ (x : Unit) -> x) unit"
unit : Unit

Check a recOR in checking position against a known expected type: each branch is checked against that type under its guard tope, followed by the usual pairwise coherence and the coverage obligation. Passing a restricted type pushes the boundary into every branch, so a branch hole reports the faces it must meet (under its tope) instead of the bare underlying type.

Under a branch guard, the faces belonging to the other (mutually exclusive) branches become disjoint from this branch's tope context, so they are pruned by pruneVacuousFaces before the branch is checked. Otherwise a face like i ≡ 1₂ would be reported as vacuous while checking the i ≡ 0₂ branch against A [i ≡ 0₂ ↦ a, i ≡ 1₂ ↦ b] — which arises in particular with flat-discrete cube variables, where i ≡ 0₂ ∧ i ≡ 1₂ is provably ⊥.

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.

Apply the renderHideTerm policy to a cell's render data: drop the <title> (the full term) from every cell, and blank the visible label of a proof-coloured (interior) cell. Boundary cells (coloured otherwise) keep their given labels. A no-op when not hiding.

Render the goal cell for a (shape) type: introduce an abstract inhabitant and render it with the proof term hidden. Under a boundary tope an abstract inhabitant of an extension type reduces to the prescribed face value, so the cell shows its given edges with a blank interior — the shape to inhabit, not an answer. Nothing for a non-shape type (a 0-cell or a non-cube goal).