)]}'
{
  "commit": "c20d7fa978c795756a7aaada5495d0c4e82ec408",
  "tree": "268b7aeee990cf9b0a0fd7b630d38d9fece2ad1c",
  "parents": [
    "230f33570256016e658abe48cca9a08e411d9f4b"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jun 25 13:35:48 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jun 25 13:41:24 2024 -0700"
  },
  "message": "fix: `IndPredBelow` should not add auxiliary declarations containing `sorry`\n\nIssue #4535 is being affected by a bug in the structural inductive\npredicate termination checker (`IndPred.lean`). This module did not\nexist in Lean 3, and it is buggy in Lean 4. In the given example,\nit introduces an auxiliary declaration containing a `sorry`, and the\nfails. This PR ensures this kind of declaration is not added to the\nenvironment.\n\nCloses #4535\n\nTODO: we need a new maintainer for the `IndPred.lean`.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b4bd9bc25a991a3e9caa4a7bf4cf27c1beb67996",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/IndPredBelow.lean",
      "new_id": "b9fc37fc5387a3daf4cafaafccef09aa9ea72c02",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/IndPredBelow.lean"
    },
    {
      "type": "modify",
      "old_id": "4e6eea6d045981f80e629512251c773c5296373e",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/Match.lean",
      "new_id": "896c4be7de168094bcd475d0f78c2570889fd1b4",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/Match.lean"
    }
  ]
}