)]}'
{
  "id": "c11aae9c7f3e125494a9b2855ad5ae0ba4547d14",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "97cb28c8f384f3fa935dbdaa4b85682c98db95f5",
      "name": "Basic.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "eb113feaf7afd8a86a21aee29606c7b642367ccb",
      "name": "Macro.lean"
    }
  ]
}
