)]}'
{
  "commit": "3d9ade01b216550fad2453cee69ca0a35b4b376b",
  "tree": "5da86fcdd38095eeeacdc1bd2697e95f7a63235c",
  "parents": [
    "ac6a29ee834ba7fd30e9372e51493d7741e9c657"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Jan 20 20:58:39 2025 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Jan 20 20:58:39 2025 +1100"
  },
  "message": "feat: align List/Array/Vector.count theorems\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "8228b236b39efeafc44db53ee4e194adc80487ab",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Basic.lean",
      "new_id": "62d154f038836f39db2eae42f0710c8662aab21e",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "7ff5af639445ee5c8d97c7d27c8cab8982826217",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Count.lean"
    },
    {
      "type": "modify",
      "old_id": "f131327840199f3d2e47a0438a80600b4863bdee",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Lemmas.lean",
      "new_id": "b41356c67131bc13d4730a2bc7f104b2adb7379a",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "e8086796157d18d6e388476f595e2d37f4e5115f",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Count.lean",
      "new_id": "28e5584404b315712ab687ac7c877fa463448c59",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Count.lean"
    },
    {
      "type": "modify",
      "old_id": "9f2d4667c30f3a2d99d8ce65b41b1bda642e9eb8",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Erase.lean",
      "new_id": "1f257fc81a6ee50b248e575581c000a144364442",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Erase.lean"
    },
    {
      "type": "modify",
      "old_id": "dd9c73ccf2799b74f7a71fdbde0fcd296a384a67",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Find.lean",
      "new_id": "058f6b1992bfc1287f0ccd754bff9e3e0f1fb323",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Find.lean"
    },
    {
      "type": "modify",
      "old_id": "9e32effb6fdd1da4896c79e6195ad5a422954627",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector.lean",
      "new_id": "c736d20f492efa87170c1269a10131c59d1c66b9",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector.lean"
    },
    {
      "type": "modify",
      "old_id": "a12414dba56848a07a3eea2ae673adb6b7e2007f",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector/Basic.lean",
      "new_id": "6deb7b0197dd98c5f3010995743b4e42eb2bfc83",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "a68512ced99ee4a2a38230083b8381e32f6a2e56",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/Count.lean"
    },
    {
      "type": "modify",
      "old_id": "859f7b6b0abffbe5c8830e36677cde4dc980d241",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector/Lemmas.lean",
      "new_id": "d818ffdaca52e33525d27a35f0da1a217e7bd395",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/Lemmas.lean"
    }
  ]
}