)]}'
{
  "commit": "0eaf79b48cfbfacbbcd2e26b2cbf8e1ffbeb4e02",
  "tree": "05cb2e0de133f9c4b5630e1787cf2902ef397007",
  "parents": [
    "d748b0c8c95c56adfb3c7cb3e4907105355610c5"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 22 19:17:41 2025 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 22 19:25:16 2025 -0700"
  },
  "message": "feat: `grind` \"silent\" `have`\n\nThis PR implements the `have \u003cident\u003e? : \u003cprop\u003e` tactic for the `grind`\ninteractive mode. The proposition is proved using the default `grind`\nsearch strategy. This tactic is also useful for inspecting or querying the\ncurrent `grind` state.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "908b88444688c519a54d6478924c7b00dc0b000f",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Interactive.lean",
      "new_id": "8fa3d3c2f8899c8f20efb500c03f17c7883954f8",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Interactive.lean"
    },
    {
      "type": "modify",
      "old_id": "60d4d270883d73caf9b3220651bbd153527c64ec",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Basic.lean",
      "new_id": "5ebacd1fc103eb138bef2f73116d6d7351f5e168",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "59a87188ad1211852a6193905900df86d71d9569",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Have.lean",
      "new_id": "f5dcf3c145a9055cad790ecac3e17fc16a7465bc",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Have.lean"
    },
    {
      "type": "modify",
      "old_id": "0571870a4fca65fcb5a03adf7c81c52cd1353f1c",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/RevertAll.lean",
      "new_id": "e91cc6154dd10086dc6fd7d5ca907637562570c0",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/RevertAll.lean"
    },
    {
      "type": "modify",
      "old_id": "6fc110ba5a597c51b790cb31561348a250e70347",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_interactive.lean",
      "new_id": "dc21b0c7852b492d075fdb38e1e04d78d32ac5f7",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_interactive.lean"
    }
  ]
}