)]}'
{
  "id": "3a9769e9c0f23b7709faed71f61e10c5889be38c",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "1fcb1529f8e5e43037c4710ce09da0becd28823a",
      "name": ".gitignore"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b577ecc33e0ed7d4123126a63a78653f3aa91b9b",
      "name": "BoolExpr.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d64479f4942df0c8eee406973a8c53c39c438060",
      "name": "SUMMARY.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "6481909ef90c9bf53adc8f63bf32d31ad77a02b4",
      "name": "alectryon.css"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d503e0fd24ed9ea2a110f92b15abb2631ce4f907",
      "name": "alectryon.js"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "09201ce55844a6ee0ae60b791541286fd0e37c46",
      "name": "bin"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8b481f25a473b15c36e4c677fa8db0511ec67975",
      "name": "book.toml"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3d7bb6cfd32cc11895f0f40137a6ad3d4d3f6ac0",
      "name": "bool.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "2b0f6ed9d1f55352b3d60efc2702dc53f252de4c",
      "name": "declarations.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "57e5bd97c4b56ba95f056c19cd51453000f3950b",
      "name": "definitions.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a8254c1d3f50472558ecd407309adf795b6b6c16",
      "name": "dep.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a7c59329461c3111d12a1d551b17bb22b8b4e9fe",
      "name": "deptypes.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "46556cdb2b4840ba5f25fdc19caf6f4c5d3620f4",
      "name": "dev"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "cdecaae83562e75c3e1bc354785e50c02e25e3f0",
      "name": "examples.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "a385e0766ee061a437940cb2d9a9f021b4d32a81",
      "name": "examples"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b8a9bb8910541cb36700507c26f75d4a35f8718a",
      "name": "expressions.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "9ae981375502ea5d2a9c778e30931779a702daff",
      "name": "faq.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "da279454f6d7d3db9d986ab45c27d6c1adc28abd",
      "name": "flake.lock"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "4edef9e4a834abe3abcc2f5d6b9f27f3ca40d33d",
      "name": "flake.nix"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "76e613884cb94f5b1392b6978b68e511c76c2d45",
      "name": "fplean.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f63b4afe7f4ecad739f4d61792816ff1ba3c8310",
      "name": "funabst.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "34bf0e1466b404ef1280b3971895c3f1653c7ea2",
      "name": "highlight.js"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "6ce4dcf6ca5ccec51144ed0641504a04d4303246",
      "name": "images"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "64696e82bf29e99064ec62a54753efdf6516ee63",
      "name": "introdef.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "8d2e29fda9fd3c5c1d354c3b3a438478dfa47ed7",
      "name": "latex"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "aad3fd05d85607f6efbbb0b7d1f8119d30c10a3a",
      "name": "lean3changes.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "27857005ef1c11b9071d637a25827404a26c5953",
      "name": "lexical_structure.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "6b9493fa6e79f9557635fbd44a780e902c38b800",
      "name": "make"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ee1b6c5d92b1585d70a3c6e1fff4429de433a669",
      "name": "metaprogramming-arith.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "0308e07b4f366c4d95f65abf58b633fc67e23c34",
      "name": "metaprogramming-arith.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "0cc211aabd06988c8063aff37a5fa11b120cd3b4",
      "name": "mission.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "09f25de2188c3ddaae26a575f8e59589f52bfcf2",
      "name": "other_commands.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "46d684b3579b375c070c9d22457a10dedebd531a",
      "name": "perf.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "9bdcad69c3e61283727928e06fcc5a74a5369234",
      "name": "pygments.css"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "afe06a296dd43177e918862a02d8f8a035b4f593",
      "name": "quickstart.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "dc6ada0f71e6024cc68547811c6865e7e821c50b",
      "name": "reference.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "10807630b9aca92a82066cbd1bbcf9cf70e60fbe",
      "name": "semantic_highlighting.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8f66e8765a90a86189a6bb6ac04a5548678eac13",
      "name": "setup.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e73a3a2e8e6d876035d9fc6fa237411708fa2e5a",
      "name": "simptypes.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "d854cb9dee73c4214c9961542b3bc05e2a88ff6e",
      "name": "std"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "961d5644a00b142218619d396ca7b6934cae00a5",
      "name": "syntax_example.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "57c493519472208e284d6100d064b3243e702a47",
      "name": "syntax_example.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f82b1b79707346843e24f32dd21e6aeff8a6d835",
      "name": "syntax_examples.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "07155e9449c0bcf1c184cbc4f37f32a9335d4069",
      "name": "syntax_highlight_in_latex.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "2b76a26167c01102380e8159fbbb8772f501ca86",
      "name": "tactics.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "010bf4076f536f4d6e6c8213bd791b518ffe526b",
      "name": "tour.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "fac1006719cca067596a99ac912ce229c498c545",
      "name": "tpil.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f9ee7145bf1d43ccf6dbd2147e7d9a4d938a9e70",
      "name": "typeobjs.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "2d8fd6763abbe32120848adf458ef1b52767e920",
      "name": "types.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a9b4c8233bd0476dc4bc8f2643bd1e169a573203",
      "name": "using_lean.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ce1491997856bf0cdf80a43de34e2417bd697a51",
      "name": "whatIsLean.md"
    }
  ]
}