)]}'
{
  "id": "5e029381de3ba117db05f1b0ad120094859f332d",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "28e2338aab1e9709e2eb1c8417ced28a224d5907",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "eb113feaf7afd8a86a21aee29606c7b642367ccb",
      "name": "Macro.lean"
    }
  ]
}
