)]}'
{
  "commit": "83ab82d29f76d5fbfa42cd180b8c8feaf455b30b",
  "tree": "4f22054a33afb5f94085b352ebe1245e10f69d6b",
  "parents": [
    "794228a982aa55cd320d5e289c80b8839f8418b0"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Mar 05 19:12:48 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Mar 05 19:42:37 2024 -0800"
  },
  "message": "feat: better support for reducing `Nat.rec`\n\ncloses #3022\n\nWith this commit, given the declaration\n```\ndef foo : Nat → Nat\n  | 0 \u003d\u003e 2\n  | n + 1 \u003d\u003e foo n\n```\nwhen we unfold `foo (n+1)`, we now obtain `foo n` instead of\n`foo (Nat.add n 0)`.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "7854c15c858a324821994e7d248a6504b22622c7",
      "old_mode": 33188,
      "old_path": "src/Lean/Expr.lean",
      "new_id": "0bdaaa4131ed731dd521d80458f25b3300a8505e",
      "new_mode": 33188,
      "new_path": "src/Lean/Expr.lean"
    },
    {
      "type": "modify",
      "old_id": "e82f4b709adc967caac013a40e815328a886144a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/CtorRecognizer.lean",
      "new_id": "3dce49a7d48270a64afedbb2b0016a7506475626",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/CtorRecognizer.lean"
    },
    {
      "type": "modify",
      "old_id": "695eb177d3b89d371014bdece13ea122e69722b6",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Offset.lean",
      "new_id": "91b3a30274cf577435bdc6b3cb288fd7370e49da",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Offset.lean"
    },
    {
      "type": "modify",
      "old_id": "ba740dc18eb290ab95e878953a05b07f5a74f429",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/WHNF.lean",
      "new_id": "63dc2b9960b8a0906123f966f31f22833cb4e10f",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/WHNF.lean"
    },
    {
      "type": "modify",
      "old_id": "4cdf7971883dc4b89e5bb3e2c270f090ab4eac58",
      "old_mode": 33188,
      "old_path": "tests/lean/445.lean.expected.out",
      "new_id": "352b58aaafc4e6e1213b30d107c9613714dcd7f2",
      "new_mode": 33188,
      "new_path": "tests/lean/445.lean.expected.out"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "b4686f0ccef33defff9f1d626a384bab2ff91acb",
      "new_mode": 33188,
      "new_path": "tests/lean/run/3022.lean"
    },
    {
      "type": "modify",
      "old_id": "5f115edef9d8284cfa511b6c8fc31db175b0b195",
      "old_mode": 33188,
      "old_path": "tests/lean/smartUnfolding.lean.expected.out",
      "new_id": "4bad259e37639c83934e26d26c826f7520cad4a0",
      "new_mode": 33188,
      "new_path": "tests/lean/smartUnfolding.lean.expected.out"
    },
    {
      "type": "modify",
      "old_id": "5b6b560a4af5cdb6dd40bacc8a7022750b37f208",
      "old_mode": 33188,
      "old_path": "tests/lean/unfold1.lean.expected.out",
      "new_id": "88c8a3cb05d62af596ac17315293fc3118478341",
      "new_mode": 33188,
      "new_path": "tests/lean/unfold1.lean.expected.out"
    }
  ]
}