linter.fugue.unfoldForeign

A definition's body belongs to the file that defines it. A downstream proof that unfolds (or simp [f]s) past the API into the body breaks together with every other such site the day the body changes — invisibly, because no two of them share a name. Characterize the definition once, beside it, and rw / obtain against that name downstream.

The linter flags an unfold f / delta f, or a simp argument naming a def, when f comes from a module other than the one being elaborated. An abbrev (a reducible tag like registerSource) is exempt — it has no body to protect.

default := false: a file-per-module check reads "another module" too literally for a development that spreads one language's definitions and the lemmas about them across a directory of sibling files (Core/ComputableTLAPlus/{Subst,FreeVars,Coercion}.lean all reason about ComputableTLAPlus.Expression.*). Deciding whether a file "is about" the constant it unfolds needs judgement; opt in per file (set_option linter.fugue.unfoldForeign true) where the API boundary is real.