)]}'
{
  "id": "5b6b61ad73ef740032cf76088b072226c9b150e9",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "96b950ea819b13d0a4e5c2ed13b1eafad4891f97",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "c7dfc1a99b66b94306607658629ae321e2f97142",
      "name": "Extra.lean"
    }
  ]
}
