)]}'
{
  "commit": "6169cf6543b1da0d51607f3ad0f39786de3eb81e",
  "tree": "d0ac846bdee8b14870c201e3e1697d0751a5c480",
  "parents": [
    "1d8555fe0bdd02c82664446309b2e167ac89c9e9"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Oct 14 15:52:31 2024 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Oct 14 15:52:31 2024 +1100"
  },
  "message": "feat: upstream List.mapIdx, and add lemmas\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d0d53d65cd21d776c0d0a7b400516bf6ca7d6a58",
      "old_mode": 33188,
      "old_path": "src/Init/Data.lean",
      "new_id": "5034afda0e4d1f16e9882d9949c7c195a7fbb931",
      "new_mode": 33188,
      "new_path": "src/Init/Data.lean"
    },
    {
      "type": "modify",
      "old_id": "e1a746a7b18e5ac9638d7c801d701cf5e6a6d5bf",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Fin/Lemmas.lean",
      "new_id": "562b26bef8a2313ed9628c863cad75df076da98d",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Fin/Lemmas.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "090fb1a6c86846fe4d913dd05591eb53f44f0ec6",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Function.lean"
    },
    {
      "type": "modify",
      "old_id": "e00a18706fbb0d3bd3164e1ca2941cb799dd5b6c",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List.lean",
      "new_id": "1ac4880a6f204fec9bebe3653d423d022d45e6c6",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List.lean"
    },
    {
      "type": "modify",
      "old_id": "e67beaa7004d18f666af724ae52c73673bcf9bb7",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Basic.lean",
      "new_id": "6ca67340f92000a62b7aea906f5f184f2064765d",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "375de39171dcf5848c206722c25bb4964b9a0adc",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Lemmas.lean",
      "new_id": "c665facf6bc07a7dae1de5ef42238a665ba37b04",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Lemmas.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "f42e2840d49b1b5b086f11bc9311f2bf2aa9cd93",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/MapIdx.lean"
    },
    {
      "type": "modify",
      "old_id": "ed9f693051d0c2beb5c91a6ed7434dae7fd7e82b",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Nat/Range.lean",
      "new_id": "74c8c1f7827e278c414e9199255265001a118145",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Nat/Range.lean"
    },
    {
      "type": "modify",
      "old_id": "e53e859713f161128ec585293b4e885949d4ae1d",
      "old_mode": 33188,
      "old_path": "src/Init/Data/List/Zip.lean",
      "new_id": "59e3691b7a5ac9563ed7997e8a990576fe089e65",
      "new_mode": 33188,
      "new_path": "src/Init/Data/List/Zip.lean"
    }
  ]
}