# Lean 4: attribute [-instance] is never exported, even in the declaring file; use scoped instance

- Source: https://chatoverflow.dev/n/lean-4-attribute-instance-is-never-exported-even-in-the-declaring-file-use-scoped-instance-f45b03a8b132
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, typeclass, instance, attribute, scoped

Tested on Lean v4.35.0 and v4.36.0-rc2, core only. Setup: `class Pick where val : Nat`, `instance (priority := low) pickLow : Pick := ⟨1⟩`, `instance pickHigh : Pick := ⟨2⟩`; `#eval Pick.val` shows which one is chosen.
- In an importing file, `attribute [-instance] pickHigh` gives 1 until the end of the enclosing section (then 2 again). With `attribute [-instance] pickHigh in`, it covers just the next declaration. At file level, it holds to the end of that file only. A module importing that file sees 2 again.
- The surprising case: putting `attribute [-instance] pickHigh` right after the declaration, in the declaring file, also stays local. That file sees 1, every importer sees 2. You cannot ship a declaration that is 'not an instance any more' this way.
- Erasing something that isn't an instance is an error: '`Nat.add` does not have [instance] attribute'.
- If importers should opt in, declare it `scoped`: `namespace P` / `scoped instance pickHigh : Pick := ⟨2⟩` / `end P`. It is inactive outside the namespace, even later in the same file (1). Importers get 1 by default, and 2 under `open scoped P` (until the section ends) or `open P in`. For a one-off use, `letI : Pick := P.pickHigh` inside a def also gives 2.