)]}'
{
  "commit": "aa83bcd070742a0c5b515bd5531fb67a1138bcbc",
  "tree": "24a778c68a645bdd09ffa8136b41c8b6cf5e6ea1",
  "parents": [
    "1126407d9b8358248ccf2f6bdc36787633c40887"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Nov 22 14:43:00 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Nov 22 14:54:45 2024 -0800"
  },
  "message": "fix: nontermination while generating equation lemmas for `match` expressions\n\nThis PR fixes a non-termination bug that occurred when generating the\nmatch-expression equation theorems. The bug was triggered when the proof\nautomation for the equation theorem repeatedly applied `injection(` to\nthe same local declaration, as it could not be removed due to forward\ndependencies. See issue #6067 for an example that reproduces this issue.\n\ncloses #6067\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "36ca4555fd236a1afc4beb8aca3b05c31aead7ec",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Injection.lean",
      "new_id": "aef74f79fd5db501710b01bc8e3454fb4ac07c86",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Injection.lean"
    },
    {
      "type": "modify",
      "old_id": "8138704437521195840e14bde660f2a6169fd5f4",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/MatchEqs.lean",
      "new_id": "824f993010acd76fd058aeba49f4dc31697322df",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/MatchEqs.lean"
    },
    {
      "type": "modify",
      "old_id": "f45ccee1696d013175e02afd2c0b1f1a9c845d30",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Injection.lean",
      "new_id": "0b61cd29f14684fa2345f9b6cd2079d0f76fb7a6",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Injection.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "821723d00ce5bde835af01bcd2f8217b32197b93",
      "new_mode": 33188,
      "new_path": "tests/lean/run/6067.lean"
    }
  ]
}