)]}'
{
  "commit": "c5d8a378ba77d655e25c55f1fcf8d1dfe9ee12e1",
  "tree": "376b7ae8d588ac22a55ec1851abdf41e6b46b841",
  "parents": [
    "2c87905d77b707c3283c1de759fd63269ac386a1"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Dec 31 09:26:33 2024 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Dec 31 09:26:33 2024 -0800"
  },
  "message": "feat: instantiate ematch theorems using assignment\n\nThis PR implements `Grind.EMatch.instantiateTheorem` in the (WIP)\n`grind` tactic.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "f20bb701ea03dc0b3ad46d2eb4c1955dd65128f0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind.lean",
      "new_id": "92019df59e8b76f6629d91d21f750034f9f89787",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind.lean"
    },
    {
      "type": "modify",
      "old_id": "a96f107d01da0a46415737f89b1f0924859a8d2e",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean",
      "new_id": "5ca3b7aaa9dd0cdaea2ae03ba3ba562622bfecd7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean"
    },
    {
      "type": "modify",
      "old_id": "82f59e81d926c8fe8b211143e5a08f8933ca4c63",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean",
      "new_id": "f8626bef0a7c7ce8efedc8f400c50c805a959c77",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean"
    },
    {
      "type": "modify",
      "old_id": "20c9a0c340dfd744c9fa88c8e27163d2d59ae056",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_ematch1.lean",
      "new_id": "f8a0a9d241c9b9e67dd09fa59a522b7a799716ca",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_ematch1.lean"
    }
  ]
}