)]}'
{
  "commit": "5482be42982b7571287b04092d42d3c19b033752",
  "tree": "efaed151a742201441447c2b5ecad2af0e0a120c",
  "parents": [
    "412389f71f8a24307e3adba69b38b4b685b04f72"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Feb 04 23:01:12 2025 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Feb 04 23:01:12 2025 +1100"
  },
  "message": "feat: align List/Array/Vector.insertIdx lemmas\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "2a91c25595668c5b9babe5f66fb4c15c3f4d812e",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array.lean",
      "new_id": "c31c9ebcf959709526a470c93891dec5f2ce78e0",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array.lean"
    },
    {
      "type": "modify",
      "old_id": "f656f988a0477a25d520d94b0130eb87bb63a4b4",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Basic.lean",
      "new_id": "c0c37b82991154239210f90a987b059544df1592",
      "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": "f2a35a8b28a4ff596f1d57d46903dcdee9fe09b5",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/InsertIdx.lean"
    },
    {
      "type": "modify",
      "old_id": "ab86095a05c50e48395a81de6055fb394b3c9e3a",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Nat/InsertIdx.lean",
      "new_id": "9d6672641ebfeb2c75f3fa980cda094f5ece1443",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Nat/InsertIdx.lean"
    },
    {
      "type": "modify",
      "old_id": "f97b8951f8c7f65f1414f48b2231cde57c313479",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Nat/TakeDrop.lean",
      "new_id": "ffc109e56d29e624670e0ea43b71f11bcd981d06",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Nat/TakeDrop.lean"
    },
    {
      "type": "modify",
      "old_id": "4a87969b88d3a258d023f98e9a4ccfd8b7b4dfb1",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/TakeDrop.lean",
      "new_id": "4ec41f858066d66421de9ca38dd155469f229607",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/TakeDrop.lean"
    },
    {
      "type": "modify",
      "old_id": "c620ef6fe532532df8194f262241e2e5be10fa7c",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/ToArray.lean",
      "new_id": "5ed2e511c6327963d348d62138bab6736cededa3",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/ToArray.lean"
    },
    {
      "type": "modify",
      "old_id": "dfd52707c549917ff3975cba71397beeb24dd922",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector.lean",
      "new_id": "194dd6db36e0d8ca59fdeb5764805224db2955b1",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector.lean"
    },
    {
      "type": "modify",
      "old_id": "3b156f81dad81ebd44f2816d52203fbd9cfbb277",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector/Basic.lean",
      "new_id": "8da7af928e16b0161bb50ea400e0d0c6e0ae519d",
      "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": "27dfe5a661bb6a255e8a07138d90a33fcd9c926a",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/InsertIdx.lean"
    },
    {
      "type": "modify",
      "old_id": "45edc49dcc078481ac8e4e4904e43e37043a086c",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Vector/Lemmas.lean",
      "new_id": "89058e8a0cba96609f4c36f9f1beb2bc884c9618",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Vector/Lemmas.lean"
    }
  ]
}