)]}'
{
  "commit": "ee260a0dbf84876ac8e4b9a00e48f35fe9f6f0bc",
  "tree": "17cc73fe76c65b6308a33b19a29fd85c73ee9040",
  "parents": [
    "0a8abcb19f7daf70ac75e5899ee3fd42f54adb33"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Jun 25 08:10:23 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Jul 17 16:10:46 2026 +0000"
  },
  "message": "fix: don\u0027t expose `inferInstanceAs` wrapping aux defs for non-exposed types\n\nThis 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).\n\nThe 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\u0027s exposure.\n\nCo-Authored-By: Claude Fable 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c96e2f32dd427549ea6a30bf304f0fbb9d0b7a6e",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/BuiltinTerm.lean",
      "new_id": "e1c9983e6c4e424e60656dbab9764581f13babe3",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/BuiltinTerm.lean"
    },
    {
      "type": "modify",
      "old_id": "d5c6d4bf86de09eb83908509cbc19b387f8cdc38",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Closure.lean",
      "new_id": "d79b11305a72de47239f292e73a2aedc43c518fd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Closure.lean"
    },
    {
      "type": "modify",
      "old_id": "2b07c1daf54f506e74ae6cf247065bcc44975708",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/WrapInstance.lean",
      "new_id": "cf7c8fcdc0d0af6a7fe21b92edaf81fbeb4178fa",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/WrapInstance.lean"
    },
    {
      "type": "modify",
      "old_id": "2360bd5d2495c65c3b2bf75f88d27518ede49320",
      "old_mode": 33188,
      "old_path": "tests/elab/inferInstanceAs.lean",
      "new_id": "a5fc6147ce258117915ec988c9f427f886202363",
      "new_mode": 33188,
      "new_path": "tests/elab/inferInstanceAs.lean"
    }
  ]
}