)]}'
{
  "commit": "607935941f2725f0fddb1b046825e59965393b96",
  "tree": "5ac5cbf936ea56f50f4776610b1e41c5e87b8c4d",
  "parents": [
    "4eaaadf1c107c6f9fabe8b0dc2f98c2f495fbae6"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Dec 27 19:17:45 2025 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Dec 27 19:19:24 2025 -0800"
  },
  "message": "feat: add `instantiateRevBetaS`\n\nThis PR implements `instantiateRevBetaS` which is similar to\n`instantiateRevS`, but beta-reduces nested applications whose function\nbecomes a lambda after substitution.\n\nFor example, if `e` contains a subterm `#0 a` and we apply the substitution `#0 :\u003d fun x \u003d\u003e x + 1`,\nthen `instantiateRevBetaS` produces `a + 1` instead of `(fun x \u003d\u003e x + 1) a`.\n\nThis is useful when applying theorems. For example, when applying `Exists.intro`:\n```lean\nExists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p\n```\nto a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables `?w` and `?h`.\nWith `instantiateRevBetaS`, the type of `?h` becomes `p ?w ∧ q ?w` instead of\n`(fun x \u003d\u003e p x ∧ q x) ?w`.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "9519aa70f527ee7d381ff2ac2481147cb7ddbfc5",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/InstantiateS.lean",
      "new_id": "37377fbd8d8de59cc8c88af2324347b23c7b6d6d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/InstantiateS.lean"
    },
    {
      "type": "modify",
      "old_id": "0c5b2acf7e114e3801970e7a589c9a3936bdac3a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Pattern.lean",
      "new_id": "82868511d8eae74ea5a5609980459b8da7dc3df7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Pattern.lean"
    },
    {
      "type": "modify",
      "old_id": "5938e83dacd792d75e8ced695f92f10356ea4c44",
      "old_mode": 33188,
      "old_path": "tests/lean/run/sym_pattern.lean",
      "new_id": "4c727a4ced693cc527d72d699b7e2f3029ee49a9",
      "new_mode": 33188,
      "new_path": "tests/lean/run/sym_pattern.lean"
    }
  ]
}