Module relevance 

Argument relevance: which arguments of a definition cannot change what it computes.

When two applications of the same definition are compared, Lean’s algorithm first tries the arguments pairwise and only unfolds on failure. Comparing an argument the definition never uses can cost arbitrarily much (Arena perf/discarded-argument: two numerals evaluated in Θ(n²) only to be thrown away). An argument position i is ignorable when either

• the definition’s value, after its leading funs, never mentions parameter i, and the rest of its type does not depend on it — unfolding substitutes into a body with no occurrence of the parameter, so c … aᵢ … and c … bᵢ … unfold to the same term whenever the other arguments agree; or
• the parameter’s type is a proposition — two proofs of definitionally equal propositions are definitionally equal (proof irrelevance), and the propositions are equal whenever the earlier arguments are.

Both facts are properties of the settled constant (and, for proof-ness, its universe arguments), so they are computed once and shared by every declaration.

Structs

Cache

Relevance facts, keyed on settled constants only.

Signature

What a settled constant’s type says about its applications, at one universe instantiation.

Constants

MAX_TRACKED

Positions beyond this are always compared.