)]}'
{
  "id": "6f38cf94806d45a1e12f30e4057b06d14e89fa88",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "9676b349dc74e8120b624b2f435926492a0f6559",
      "name": "Attach.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "55c3e3fe0094015bdf96df0b81431306660422e5",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ba1ef50afde9946d08e527df698d8f7434aa0dce",
      "name": "BasicAux.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "5145813dc4bd7316f0c5034c19af821bcfecb0ae",
      "name": "BinSearch.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "9608cb89e6a6de0450e640c0d217fdc726c5073d",
      "name": "Bootstrap.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b389124f42e6462cd19d1ade18f77f7cf9d1415d",
      "name": "Count.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e383c7764a8b8fef0e06a43b15a26f945f88db47",
      "name": "DecidableEq.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "95a9a26a4269e5f0d4fbd343345f85cf8cf1430b",
      "name": "Erase.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "1976c105e9709001ac69885a9e065349825c6afc",
      "name": "Extract.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c6e4279b4d5c9472dcd95d8d52e78e4c58efaf1c",
      "name": "FinRange.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "36c08123d500f674bcac0c33b1b31c809955d6dc",
      "name": "Find.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d95c8fced6a720e8285076d01ce6949825316c50",
      "name": "GetLit.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "83d1b22e4f645fdd7ce67f42440d5325120b0d1d",
      "name": "InsertIdx.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "1c2072563bcadf09ff636b68e3c4ee0c57a61696",
      "name": "InsertionSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "19a33ca9339deb4d237529942df418b060e801e4",
      "name": "Lemmas.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a700084e4b3df55d8e1a8265ebc6e1f89d6aa309",
      "name": "Lex.lean"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "668da8b8e724028b9a16be2bebd48a27326e568e",
      "name": "Lex"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a9164f4eeea911f27b892acfbb21513c8c7f9195",
      "name": "MapIdx.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d59053472ce683e6ebd93141819875ee8d956cbe",
      "name": "Mem.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b59b4f7dec97805ad4a366622e19a9d8f94397c5",
      "name": "Monadic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "88b046e4edee6aa16d7abbef210f8a626ffb5885",
      "name": "OfFn.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "2d2ab764dfad65f9a8a3363fc2107f8e1b655ff3",
      "name": "Perm.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b4ee01fb3fd394ead8d319607ca5c2ac127588c5",
      "name": "QSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "af9abfc26a5e45be4784e5a98919c0c3f1a93ffd",
      "name": "Range.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "85c40e84ff69f8e7da6fbfa176bce0a9faeed80d",
      "name": "Set.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "aa50e66555beec4e22a0e531e9f14feae7ee5f28",
      "name": "Subarray.lean"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "fa78fed93ab04cbb09d371319ce8d47af7d7c71d",
      "name": "Subarray"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "09d3c47c367e7fae16f12847295e7a9422464d18",
      "name": "TakeDrop.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "9fea34d774af085fd305003d0ecc88c96d870412",
      "name": "Zip.lean"
    }
  ]
}