lint def unfoldings

Stream: lean4

[James Gallicchio]

I know this has been discussed before but I can't remember the right keywords -- is there some way to lint for proofs that rely on unfolding a given irreducible def in the kernel?

I recall some discussion about having a primitive way to seal a def within a specific API, in a way that even the kernel doesn't look through. If anyone finds links to that prior conversation I'd appreciate it.