)]}'
{
  "commit": "1c0a508a9b9e2467d66c04fee0355c2d7a1e49e2",
  "tree": "3a73aecc45bac1553b0efe77d9ca6b55e2e93ccd",
  "parents": [
    "ba9237e196e4f6fa353c605230d81b7d9582d49f"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 04:54:28 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 04:54:28 2026 +0000"
  },
  "message": "fix: queue structure eta equations in `grind` internalization\n\nThis PR fixes an internal `grind` error (\"term has not been internalized\") caused by structure eta.\n\nWhen internalizing a structure-valued term `a`, `propagateEtaStruct` internalized `⟨a.1, ..., a.n⟩` eagerly. If `a` is the argument of a projection `a.i` that is still being internalized (e.g., `a :\u003d g y` while internalizing `(g y).val`), this term contains the incomplete application `a.i`, and the solver hooks receive it with missing arguments. The fix adds `ToProcessElement.internalizeRhsAddEq` and uses it to queue the eta equation until no application is in progress.\n\nCloses #16101\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b63bd5474f18b02d351716aa7efa094ad7883e89",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Core.lean",
      "new_id": "9952112548f24363b8b0372a4d809ff7bfedcb43",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Core.lean"
    },
    {
      "type": "modify",
      "old_id": "ca67bab725654622f333e8c01e7d906b6ac0c46d",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean",
      "new_id": "e1b1d1611ba4a51a59154daf7a16d510e18573ba",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean"
    },
    {
      "type": "modify",
      "old_id": "6cd883cd4fc9c5e6bcbdb715d53b8bd0f75cba70",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "eb3ed33ea3ce4abaf4c63a29dd13ebafa08a42e9",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "56c35230dad621fe44101353954639885e1bdd47",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_16101.lean"
    },
    {
      "type": "modify",
      "old_id": "f8cfc49ddad9119d4dd198186d1507a87f6e7e6c",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_norm_levels.lean",
      "new_id": "e658ae0e192ef64e50abf23bfdb274ca270e7c9c",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_norm_levels.lean"
    }
  ]
}