fix: don't expose `inferInstanceAs` wrapping aux defs for non-exposed types This PR fixes `inferInstanceAs` marking its wrapper auxiliary definitions `@[expose]` even when their bodies are well-typed only in the private scope, which made instances defined via `inferInstanceAs` for types without an exposed body publicly ill-typed (fixes #14147). The wrapper aux defs keep their public name and exported signature so the exposed instance can still reference them, but their bodies are kept out of the public scope unless the instance type and the expected type are also definitionally equal in the exported environment. `mkAuxDefinition` gains an `exposeBody` parameter and `wrapInstance` an `exposeAux` parameter; the `deriving` code path is unchanged because it already runs the entire derivation under the exporting scope matching the derived instance's exposure. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.