)]}'
{
  "commit": "da33e537e266180da124f7af0c16504da3ce3bae",
  "tree": "115c601ee89fe14559ecb81e96afaa835b9bc635",
  "parents": [
    "82e49ffd124de5e95e7ff8b7755040120832173d"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Aug 26 22:21:24 2025 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Aug 26 22:21:24 2025 +1000"
  },
  "message": "feat: lemmas about rounding dyadics\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "fc3b7772c284d7a42f15e36dfd484c120c3f9cd4",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Dyadic.lean",
      "new_id": "7bc7bc55fff9b3520bcf3a03d30ef2cd472deac3",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Dyadic.lean"
    },
    {
      "type": "modify",
      "old_id": "fb294897b4e1f44d6a7a68a12b827c5d398f1168",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Dyadic/Basic.lean",
      "new_id": "e9b0e4c37373f32b2f855a29a3fdb5d8dbef0575",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Dyadic/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "cf4964ba3b80fac0785a881eb690027de12b6b74",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Dyadic/Round.lean"
    },
    {
      "type": "modify",
      "old_id": "ad0a8d1be25fed61748c7dfcd5cb71fefe758546",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Rat/Lemmas.lean",
      "new_id": "97cfa428fcf180864e38ed7d314fe4aa6315d24b",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Rat/Lemmas.lean"
    }
  ]
}