)]}'
{
  "commit": "e6c460e5f4cfc341afe19514b05c80f5c42a3240",
  "tree": "2a8cdf2b60bea5789fa9ed051242bf9da150c48a",
  "parents": [
    "7fbe8e3b36faabc9cfcc45e65a4b7ef042c0b068"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Nov 20 17:47:51 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Nov 20 17:47:51 2024 -0800"
  },
  "message": "fix: nontermination when generating the match-expression splitter theorem\n\nThis PR fixes a non-termination bug that occurred when generating the\nmatch-expression splitter theorem. The bug was triggered when the\nproof automation for the splitter theorem repeatedly applied `injection` to\nthe same local declaration, as it could not be removed due to forward\ndependencies. See issue #6065 for an example that reproduces this\nissue.\n\ncloses #6065\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d3cfd47ae7bf7d111b43c69492fb915714ac0092",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/MatchEqs.lean",
      "new_id": "d9151522e11cf44a92bdaba4af61f20136396d2b",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/MatchEqs.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0325e8fdc7f8c51bac680d149b15236376a4057f",
      "new_mode": 33188,
      "new_path": "tests/lean/run/6065.lean"
    }
  ]
}