)]}'
{
  "id": "03f924befa6f519b6fc4e39172c0264b60a94593",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "16a28bc643a8e886e143c6ea9bba86c40b40b5fe",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "dbaf6896042988d285b4aeaf78b2969fe94900fa",
      "name": "Extra.lean"
    }
  ]
}
