)]}'
{
  "commit": "a6240a983fe4ffcf6eb9a6d755df96e0a288e197",
  "tree": "e7756030921dd912bec2bd3e1c7f15558c1534f9",
  "parents": [
    "6e02421ae3a8e0862208c379e87929f15ec39123"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Apr 23 09:38:49 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Apr 23 10:44:39 2024 -0700"
  },
  "message": "fix: improve `isDefEqProj`\n\nThe new test `3965_2.lean` shows that `tryHeuristic` is also useful\nwhen solving contraints of the form `t.i \u003d?\u003d s.i`. For example,\nsuppose we have `(f a).i \u003d?\u003d (f ?u).i`. By using `tryHeuristic`,\nwe obtain the solution `?u :\u003d a` before unfolding `f`.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c4546d3eed50e239fb5de4de30017e3deaf94d0b",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/ExprDefEq.lean",
      "new_id": "8da28164f60bc03898c6755cdae66408f95f0bb2",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/ExprDefEq.lean"
    },
    {
      "type": "modify",
      "old_id": "4b1bf03a84d9833e227c47cba9ca25d95e10bf55",
      "old_mode": 33188,
      "old_path": "tests/lean/run/3965.lean",
      "new_id": "35c4500f1b947797e9b434164b24d058de1b4d89",
      "new_mode": 33188,
      "new_path": "tests/lean/run/3965.lean"
    },
    {
      "type": "modify",
      "old_id": "5b04aacef36b61d12eb2dc54d5add8925b0fd1a3",
      "old_mode": 33188,
      "old_path": "tests/lean/run/3965_2.lean",
      "new_id": "ee0df78c2587243e27aa9060b0a6dd6f339961a4",
      "new_mode": 33188,
      "new_path": "tests/lean/run/3965_2.lean"
    }
  ]
}