)]}'
{
  "commit": "7fd2aa04ae1dd02e7f8a2cb5ceacb7fbebbbb48a",
  "tree": "df478e0005f1b6ca36036609f4e0cc25c9f94618",
  "parents": [
    "47e0430b07cdd2569046e531fb44eba5f6ffc3d0"
  ],
  "author": {
    "name": "Tobias Grosser",
    "email": "tobias@grosser.es",
    "time": "Sun Oct 13 21:11:31 2024 +0100"
  },
  "committer": {
    "name": "GitHub",
    "email": "noreply@github.com",
    "time": "Sun Oct 13 20:11:31 2024 +0000"
  },
  "message": "chore: move BitVec.udiv/umod/sdiv/smod after add/sub/mul/lt (#5623)\n\nDivison proofs are more likely to depend on add/sub/mul proofs than the\nother way around. This cleans up\nhttps://github.com/leanprover/lean4/pull/5609, which added division\nproofs that rely on negation to already be defined.",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3f9caf533ec78e5ed44b8f10610684c49b5f12bb",
      "old_mode": 33188,
      "old_path": "src/Init/Data/BitVec/Lemmas.lean",
      "new_id": "59e7e4749e03d409040653631234296b429a8626",
      "new_mode": 33188,
      "new_path": "src/Init/Data/BitVec/Lemmas.lean"
    }
  ]
}