)]}'
{
  "commit": "3b59c5c51ac70280f5e7b28fe2dc6029695c0478",
  "tree": "db636e100c047b0d5614d22f566953293e78ae5f",
  "parents": [
    "6ca23a7b8bee57152110ce500ce795148707d4ed"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Feb 13 16:28:03 2026 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Feb 13 16:28:03 2026 -0800"
  },
  "message": "fix: assertion violation in `mkEqProofImpl`\n\nThis PR fixes an assertion violation in `grind` reported at #12246\nThis assertion fails when in examples containing heterogenous\nequalities with elements of different types (e.g., `Fin n` and `Fin m`) attached to the same\ntheory solver.\n\nCloses #12246\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "a3f4af97f7f8d9f927bb815fc854f4b7daa8933c",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Proof.lean",
      "new_id": "73a6f5f56acb80952fe40534248d7694e5dc85fc",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Proof.lean"
    },
    {
      "type": "modify",
      "old_id": "ef858b0f7d50b9a80d6a79320ff3fc252d0451c8",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "6f33c9117487b909f4575b87b0f619b3dbc04e07",
      "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": "5138d036c54550293d5c8e5163b57de9a1e05bcf",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_12246.lean"
    }
  ]
}