)]}'
{
  "commit": "cbfc9313affad45012ebd5ac40b338ee829009b1",
  "tree": "c56583a6176a151ecaed4cbf918a9ec8794fb301",
  "parents": [
    "2c6a32e2f96954b5473df9c7180b582715a5293d"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Thu Dec 11 14:23:43 2025 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Thu Dec 11 14:23:43 2025 +1100"
  },
  "message": "fix: include star-indexed lemmas with `+all` when partial results exist\n\nWhen using `apply? +all`, star-indexed lemma fallback was incorrectly\nskipped whenever the primary search found any results (even partial\nones). The condition `!results.isEmpty` caused star lemmas to be\nskipped even when only partial solutions existed.\n\nNow with `collectAll\u003dtrue`, star lemmas are searched unless a complete\nsolution was already found. Results from both primary search and star\nsearch are combined when `collectAll\u003dtrue`.\n\n🤖 Generated with [Claude Code](https://claude.com/claude-code)\n\nCo-Authored-By: Claude Opus 4.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "96c29b59944c9a6e531753cf671f9487f8ddc723",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/LibrarySearch.lean",
      "new_id": "98210263030141804c8f1303fa2179254dc3b8f0",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/LibrarySearch.lean"
    },
    {
      "type": "modify",
      "old_id": "7aa5531920c13dd2f9d47a2d663da9026ce55f18",
      "old_mode": 33188,
      "old_path": "tests/lean/librarySearch.lean",
      "new_id": "f106eae63e511bd653bb637e4fccad48e15695b3",
      "new_mode": 33188,
      "new_path": "tests/lean/librarySearch.lean"
    },
    {
      "type": "modify",
      "old_id": "bab597d2cad9aba6f987d00f8c4f310a548133b0",
      "old_mode": 33188,
      "old_path": "tests/lean/librarySearch.lean.expected.out",
      "new_id": "f55e1ca619a8e1c475c19e8b40c592d80f689793",
      "new_mode": 33188,
      "new_path": "tests/lean/librarySearch.lean.expected.out"
    }
  ]
}