)]}'
{
  "commit": "8e7dc7b3ecfd118251f61af1d6921524608d87f7",
  "tree": "5eabf51a697a77cf3da51d74b922979a9babdcbe",
  "parents": [
    "e765138bb4dc05ed563237203c9db1ba81c2c57a"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Dec 24 15:46:53 2025 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Dec 24 15:57:55 2025 -0800"
  },
  "message": "feat: add `AlphaShareBuilder`\n\nThis PR adds functions for creating maximally shared terms from\nmaximally shared terms. It is more efficient than creating an\nexpression and then invoking `shareCommon`. We are going to use these\nfunctions for implementing the symbolic simulation primitives.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "53bfd3f09dabee4aef6ace2a3b491e97ce7ea404",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Main.lean",
      "new_id": "503d2c003a8b6a8cf3086be397edbc2b23f45ccf",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "c1d5151dfecd719839f4eadc6fd15d045edf48d2",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind.lean",
      "new_id": "3592cfef9ec00b3e10406e1b70ebbd6c433343fd",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "52dd92b495be49e7c08b0f2611db8cb97f7810e2",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/AlphaShareBuilder.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0bebbb419eb92abe811ec753d5176e22dc3ed437",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_alphaShare_builder.lean"
    }
  ]
}