)]}'
{
  "commit": "3a733abe112d1093683ed5ded622457590a9c129",
  "tree": "0245c18a516905ba37cf7873b7d8ceeec32b8eb1",
  "parents": [
    "3cba17140f85f1544b48e68941918c58244851cf"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Jan 02 10:47:53 2025 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Jan 02 10:51:56 2025 -0800"
  },
  "message": "fix: congruence closure used in the `grind` tactic\n\nThis PR fixes a bug in the congruence closure data structure used in\nthe `grind` tactic. The new test includes an example that previously caused a\npanic. A similar panic was also occurring in the test `grind_nested_proofs.lean`.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "0a80f7e753385ce3e315fb35b22b3a54b3712f14",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Core.lean",
      "new_id": "747e9eb9875fd86f13291c67a1f69f2acae73e23",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Core.lean"
    },
    {
      "type": "modify",
      "old_id": "762048e1202c6b4b65a80ecaf066bdeca6a9173f",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean",
      "new_id": "1d19b860ba055c62346eafb1eec092f8eb5f3e10",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean"
    },
    {
      "type": "modify",
      "old_id": "fb4986404eb9120311a3bcd7b3988914173367b5",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean",
      "new_id": "6231923227bf6c25f07d5f61245a0b247926d0f3",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean"
    },
    {
      "type": "modify",
      "old_id": "b0e77d7a3069f83a8d7d2a9b33bb10e8e64b4ac0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Inv.lean",
      "new_id": "c09ad807e7d858a55593be013905f24fbefaf469",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Inv.lean"
    },
    {
      "type": "modify",
      "old_id": "2f62f59b72fc810cb87a7d573db90e2836abadad",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "1065c7b4d34492b9937b2d700b4fc6b2bbdd02a3",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "08d2238d17c82e091feae3575d2f69125b6554d9",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_ematch2.lean",
      "new_id": "2d4f1c850b98c1a3968848dd803bda0ca69d7a25",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_ematch2.lean"
    },
    {
      "type": "modify",
      "old_id": "12bc224f99f9d80e1becde0adeb99f4c5fa79267",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_nested_proofs.lean",
      "new_id": "bee9020b60e57d748e5bf24b9887aaa0be23272c",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_nested_proofs.lean"
    }
  ]
}