)]}'
{
  "id": "976ea9a944fad79df0249a4eb8103b9d960d819c",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "caabd1b99327da16cfa813ca50e98dbcda35adbd",
      "name": "Attach.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "23101ce8fe2d44481855b26ed001f2a7ba87b0b9",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "21f9cc3a2f4b0e18b5be7681db6ddf15415b12c7",
      "name": "BasicAux.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a3d7a488d9e166c2ca7efb2a23d9c791f6fddaa0",
      "name": "BinSearch.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b44e4588002b542dd1445339bd3d5ae7e1d9d00b",
      "name": "Bootstrap.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "567a7c25a1de2867fefe64342b23a3898a557e6b",
      "name": "DecidableEq.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c294c0b7e14b4f22b2b2e80a043b0c5191f489c4",
      "name": "GetLit.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3091baeda652cf0f75d223c33373e75c47716532",
      "name": "InsertionSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3fea6f83ef185c47cb11dd6c52a394dc58699c19",
      "name": "Lemmas.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c33251ba397021612e08c84a05ab0a9cc4c5bcdd",
      "name": "Mem.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "1f71a07bb492295a0b66161bb47d20e0f852688e",
      "name": "QSort.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "53f62af86586c76151ac2bfab0fbd565b5baffa0",
      "name": "Subarray.lean"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "b171bb8cc941da237b710459fb218622fdfe5f0b",
      "name": "Subarray"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "6b160b2e0aa441166240f25d74ed616abd2f5624",
      "name": "TakeDrop.lean"
    }
  ]
}