)]}'
{
  "commit": "0c433e56464e59bcabd4dc214886460848ac2c68",
  "tree": "d0308156b0f85e57c3404fba8728b6b65aac90d5",
  "parents": [
    "b21cef37e4b6d7ee2a2f1778cfb9a7d1bbc2c1fe"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Fri Nov 28 03:02:09 2025 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Fri Nov 28 03:02:09 2025 +0000"
  },
  "message": "fix: strip nested mdata in grind preprocessing\n\nThis PR fixes an issue where `grind` would fail after multiple `norm_cast`\ncalls with the error \"unexpected metadata found during internalization\".\n\nThe `norm_cast` tactic adds mdata nodes to expressions, and when called\nmultiple times it creates nested mdata. The `eraseIrrelevantMData`\npreprocessing function was using `.continue e` when stripping mdata,\nwhich causes `Core.transform` to reconstruct the mdata node around the\nvisited children. By changing to `.visit e`, the inner expression is\npassed back to `pre` for another round of processing, allowing all\nnested mdata layers to be stripped.\n\nCloses #11411\n\n🤖 Generated with [Claude Code](https://claude.com/claude-code)\n\nCo-Authored-By: Claude \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3422234ac32d8f003f36d9aa3aeadd49aaeb14a4",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Util.lean",
      "new_id": "d93eba35cffb0ee938abb810272dda374ce1dd8a",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Util.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "f3f52a6a12e02a3ca1f62f22ee7790e6d4f3e01c",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_nested_mdata.lean"
    }
  ]
}