Module taint 

The taint path of every assumption a refused result rests on: the declarations through which the target reaches it.

Lean’s #print axioms (CollectAxioms) names the axioms a declaration rests on and says nothing of how they are reached, so a refusal that names only sorryAx leaves the reader to find which dependency admitted a step. This walks the checked environment along exactly the edges CollectAxioms follows — a definition, theorem or opaque through its statement and its body or proof, an inductive through its statement and its constructors, a constructor through its statement, an axiom never (an axiom is a leaf: the axioms its own type mentions are not reached) — breadth first, so each path is a shortest one, and it takes a declaration’s references in ascending Lean-name order, so the path is a function of the environment alone. A declaration the importer introduced (a sharing helper, whose name encodes no Lean name) is walked through and never printed: the path names Lean declarations only.

Only the environment is read. A path is an explanation of a refusal the assumption policy already made; it never decides one.

Structs

TaintPath

One assumption and the Lean declarations through which the target reaches it, target first and the assumption last, in Lean’s spelling.

Constants

STAGE

The receipt stage whose refusal a taint path explains.

Functions

diagnostics

One disallowed_assumption diagnostic of the assumption-policy stage per assumption outside Lean’s three standard axioms that target (a kernel name, printed as target_lean) rests on, naming its taint path. assumptions are the result’s (Lean names).

taint_paths

The taint path of each of assumptions (Lean names) from target (a kernel name), in the order assumptions lists them. An assumption the target does not reach through the environment has no path and is left out.