)]}'
{
  "commit": "c44dca23eaf7a1f3142a64866c84aadca13aaca1",
  "tree": "c79218034338d9a5fa4812613e186f66a8ff8cf2",
  "parents": [
    "4600bb16fcded0356d20ae232e7f8580c56a5955"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Nov 19 12:41:00 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Nov 19 12:41:00 2024 -0800"
  },
  "message": "fix: `isDefEq` for constants with different universe parameters\n\nThis PR fixes a bug at the definitional equality test (`isDefEq`). At\nunification constraints of the form `c.{u} \u003d?\u003d c.{v}`, it was not\ntrying to unfold `c`. This bug did not affect the kernel.\n\ncloses #6117\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d4100c6bb38d17308c409a9aec5ae25b04c5295a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/ExprDefEq.lean",
      "new_id": "b22153af5273fd428a3bea2b950b70e5345d758d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/ExprDefEq.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "95bdb51e9232c30730a63eef868f9cf7152ef182",
      "new_mode": 33188,
      "new_path": "tests/lean/run/6117.lean"
    }
  ]
}