)]}'
{
  "commit": "29477b3b7c8f13f45a969baf2e3e2bec4e34f2f9",
  "tree": "9c7d5d300e30a9dd855f32ecc65180c1d20892d5",
  "parents": [
    "b54be549baf8d696bd5c70f40c8f70642d565f1d"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed May 08 13:36:22 2024 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed May 08 13:47:15 2024 -0700"
  },
  "message": "feat: add `withSynthesize (postpone :\u003d partial) k`\n\nIt forces pending elaboration problems and tactics to be executed, but\nallows TC ones to be postponed.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "5db63c556e2543dd3205e4959642effcc655f83a",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Binders.lean",
      "new_id": "9976d9141e26f10694f2656565c459c58b20d70f",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Binders.lean"
    },
    {
      "type": "modify",
      "old_id": "56cdc5e0dfaa429b80c3b5e66cb39ebd70bbe7d3",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/BuiltinNotation.lean",
      "new_id": "cca120f25ca0baa1f90262c51ff546f9011144f2",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/BuiltinNotation.lean"
    },
    {
      "type": "modify",
      "old_id": "c4acb68e1238d446a60e2eb09cfc7439ff6ef4f4",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Extra.lean",
      "new_id": "abd082cb5194b7331b7d023f354b50c62e204bc2",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Extra.lean"
    },
    {
      "type": "modify",
      "old_id": "cc7e2d688d88f96dfec0f76add5de89937c2bda0",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Inductive.lean",
      "new_id": "f73200252410bce36802a8540b9ec8475eb642b8",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Inductive.lean"
    },
    {
      "type": "modify",
      "old_id": "00ee772bfd1e8127689bc827c76403723b249cd9",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/StructInst.lean",
      "new_id": "65290fc41eefefd77819d8a7a02697f5ba67fe50",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/StructInst.lean"
    },
    {
      "type": "modify",
      "old_id": "a39d027661651fb03c131c3fe045862ea9cc3a50",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/SyntheticMVars.lean",
      "new_id": "f605436c94c68099b162863bc9a8be4f50e17a8e",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/SyntheticMVars.lean"
    },
    {
      "type": "modify",
      "old_id": "ea40cb6f0fd377758895368c01a4f3151ded0ffa",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/BuiltinTactic.lean",
      "new_id": "f7e3db804f90ec041ad96cfdabfbcc18dfe4b963",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/BuiltinTactic.lean"
    },
    {
      "type": "modify",
      "old_id": "a1171cd8f30e0242be3ee7379452ac6e0f9879d5",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/ElabTerm.lean",
      "new_id": "1d686fe6a567f7232683793db467ccb640c88b05",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/ElabTerm.lean"
    },
    {
      "type": "modify",
      "old_id": "e74577c6aea1b87efc2d434632a4a77f45f2774a",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Induction.lean",
      "new_id": "99caf6ec15940ee1c595c5364161abd110236b65",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Induction.lean"
    },
    {
      "type": "modify",
      "old_id": "bb7e5a8cf5df528fdff581da6f6ccbc8f47040f5",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Meta.lean",
      "new_id": "c6be92112e9222fbe7211f0783b4bbbd51be8d92",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Meta.lean"
    },
    {
      "type": "modify",
      "old_id": "6c3a89d4ed27be8b23a95bf78d138c6813dcd62a",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Simp.lean",
      "new_id": "a87a2ac23bc0d165ae0ea1ac227a45fdcc1631b6",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Simp.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "a36a7e498ccb1c96bb68be7d1678d30b62dc3e6a",
      "new_mode": 33188,
      "new_path": "tests/lean/run/may_postpone_tc.lean"
    }
  ]
}