)]}'
{
  "id": "84db2b7ea743136dcb590d16781c10f2a427d0ca",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "a1f0b787c37f6f6881dafc5eed5bf8ffc050cb39",
      "name": "Attach.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "4252bd32c1dd5d9b4d81f6783ce374e8690338c9",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "846183b5ab96f90ac650b78b97e2de6221b6dfb1",
      "name": "BasicAux.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c69dc8cee9ab9851726f6fcef179cc2ebd52e929",
      "name": "BinSearch.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "004f4e2c48c9e254fbd23415d0d33d978f4c2415",
      "name": "Bootstrap.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "be545d6e13eb6192c5daa13c8b8be1e43b9d82fb",
      "name": "DecidableEq.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "5d49f88027d9625252b1fc186ae001187d5c0c96",
      "name": "FinRange.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "cf522faf5355ea578e63f7e185867a48439e369c",
      "name": "Find.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f5139dc5b4d91242b9a65f95289dd5e6989c712f",
      "name": "GetLit.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "fa4c1b7a2be403c9d607317460d16de79c9bd433",
      "name": "InsertionSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "377027f08f1aacc2a77576356b5f8f188387f5fc",
      "name": "Lemmas.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "7d19d1f6f0e543743845624bfbdce39041c04916",
      "name": "MapIdx.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "284b03e58cf80b848c505e06c52db0122a02cdb0",
      "name": "Mem.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8056b54b71928ef251240c002b0095c1c71ed842",
      "name": "Monadic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a7b7d58c7ddb1f21a1405fb6e08e73318e08557b",
      "name": "Perm.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "82cd9f4b7167c0233f7f64499ec284cfb9ed2b96",
      "name": "QSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c88eb8e16446819513c87dff3edfebe1829936d3",
      "name": "Set.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3b614f9b3b6a9dfdacf999ce7288eb88b6b36bd7",
      "name": "Subarray.lean"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "3b066a24b9282ba8969da5027c08ee91c297de92",
      "name": "Subarray"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d654dd40cec28d5797047b4f9b16697f5c0c510c",
      "name": "TakeDrop.lean"
    }
  ]
}