)]}'
{
  "id": "36d1cdb148b97a26e0c45eebfff09e31ac191996",
  "entries": [
    {
      "mode": 33188,
      "type": "blob",
      "id": "1fcb1529f8e5e43037c4710ce09da0becd28823a",
      "name": ".gitignore"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ae9d02cbd4b994623fb018dc1a3c6f51308db282",
      "name": "BoolExpr.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8974ccee5accee2f53d4eee2619ef2d7ad0b98ec",
      "name": "SUMMARY.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "6481909ef90c9bf53adc8f63bf32d31ad77a02b4",
      "name": "alectryon.css"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d503e0fd24ed9ea2a110f92b15abb2631ce4f907",
      "name": "alectryon.js"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "72bbc4d3acff6d78db164b86c60beedd432c73b4",
      "name": "array.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "38442c9df0b356e1303c709e6bc32e6d4be66e4e",
      "name": "autobound.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "f21cbdb80d97a21a5cd71203ee63f5d11865d87a",
      "name": "bin"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8ff0a543342153771d97e33f84dcf9163ba0810a",
      "name": "book.toml"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3d7bb6cfd32cc11895f0f40137a6ad3d4d3f6ac0",
      "name": "bool.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "11cf1b1b090f6fc42c973edfb94ad840e4d32da8",
      "name": "builtintypes.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d012232d9db9b26c9b0024f8bca21325bf258285",
      "name": "char.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e22e3582aeaf7fb5e9d0a9efad57bd26aff4845f",
      "name": "declarations.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f203fa57cebf252e656835f0f62aad3bd7b6dd4a",
      "name": "decltypes.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": "ab76713b572b8de2a982fea249406f345c1858fe",
      "name": "dev"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "8ec1ffdab78de1dd9dcd71617df46b070815e59b",
      "name": "do.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "17e6d9f7f1064022ad71889e49a20a402dca0f1f",
      "name": "elaborators.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "bb05c235c76d882470d27acda4c24b46aa18c73d",
      "name": "enum.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "cdecaae83562e75c3e1bc354785e50c02e25e3f0",
      "name": "examples.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "bdcdf06414c756765b6ce18021c7bde2c8c9ddff",
      "name": "examples"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "51242b5d8d6a5c6ee81c5750cebab914c2509faa",
      "name": "expressions.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "319bc9ddd6d00381e97f5860099527be342041af",
      "name": "faq.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b4eeae387a31eb5cc4d1a3dc2cd3f995d5ca8db6",
      "name": "flake.lock"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ccf543d48e10312d0c6c8da5383164f0bc8e190f",
      "name": "flake.nix"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f32689c30c20ec6c7a1df4f785958471ce29affc",
      "name": "float.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "4f00130c6f0a7bad78ce858df97ea47b88025b2f",
      "name": "fplean.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f63b4afe7f4ecad739f4d61792816ff1ba3c8310",
      "name": "funabst.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "4c6600ab529e95c2bc169223c8154829176bc14e",
      "name": "functions.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "34bf0e1466b404ef1280b3971895c3f1653c7ea2",
      "name": "highlight.js"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "aa7120339585b91fa40eabe3e39d8bd0dc935088",
      "name": "images"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "0292464d19d91f7831595a5928963aeb6fb457cf",
      "name": "implicit.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f93a81fc00bcc815226c1e86d344f3199544a2f2",
      "name": "inductive.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "90cb940ce4ee6ea6c5ad69bb7a107ce04eac7125",
      "name": "int.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "64696e82bf29e99064ec62a54753efdf6516ee63",
      "name": "introdef.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "4949181a88adacab59cdebedc26ebbc75b7f0380",
      "name": "latex"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "10c41c68adaab75856a64bf37182cc2991f29885",
      "name": "lean3changes.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3b62d226bd4d635c283fd8219dc64b94a4685a83",
      "name": "lexical_structure.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "6811f7b83e870207d89ffca37fcc952e27b94796",
      "name": "list.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e69c39faec9db5fe581fdfb909ce65096b921fd4",
      "name": "macro_overview.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "7ca77f76ee31e3919d2d9426bc42a970a276dcca",
      "name": "make"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ee1b6c5d92b1585d70a3c6e1fff4429de433a669",
      "name": "metaprogramming-arith.lean"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "de03cac28fa022aba0d177cef430cd30196531c1",
      "name": "metaprogramming-arith.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "0cc211aabd06988c8063aff37a5fa11b120cd3b4",
      "name": "mission.md"
    },
    {
      "mode": 16384,
      "type": "tree",
      "id": "c61885fcbcff98427a92c26be4e40f6863bcc13b",
      "name": "monads"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "09df93d3e88edb04c82fd1888aaef0c595ec5101",
      "name": "namespaces.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "6b5cbdaf8e129d80826f82b7dde6bdd0b8d0a0ab",
      "name": "nat.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d1e1b8203bf95dacb54b5def181fee7ab8781994",
      "name": "notation.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f33af4ff3f1d31a528334023cacedb47f3ecc230",
      "name": "option.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "cdf74624608539a4fbeb341367cdee53004703f6",
      "name": "organization.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": "4c5dd396c1f24bdc9aba852593014d7eec69c438",
      "name": "quickstart.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "bb439552047153d20be224828adab02e7bcb4ff7",
      "name": "sections.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "877706c75dd0a7d04ae0ddf248c38fd5b619e7ef",
      "name": "semantic_highlighting.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "d19245b8ab1474d36e213932e7ab72088aa110ae",
      "name": "setup.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e73a3a2e8e6d876035d9fc6fa237411708fa2e5a",
      "name": "simptypes.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "ed218ce9a0db0f032f7b1be4f734afe50cc9573d",
      "name": "string.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "b40e87ea641dcbc828afa9da2a619ef77c06ee15",
      "name": "stringinterp.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "695f90214f4f84d1e41bf81034ec7ecda3650d57",
      "name": "struct.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e6a3a527c95d28cbe8ba3b9c154dc6ae127a619c",
      "name": "syntax.md"
    },
    {
      "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": "572a4410418fdfb92d3bb6f4d12ff166ee889f51",
      "name": "syntax_highlight_in_latex.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "150e3747443f7fc2836839b1a3e12389dc27917d",
      "name": "tactics.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "83a3f5dd2b6d1e341e5895e4348e37e34fea8cfc",
      "name": "task.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "3400b7668fd231d61bc5ded90ba0d13d7661296c",
      "name": "thunk.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "294f2962257c5fe259899c8c03842c6717fb1df7",
      "name": "tour.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "891d29ad3876a0199eaaef21f7f84e0276cbca21",
      "name": "tpil.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e0aec3759005c25c0434ee618e541017dc1ccd20",
      "name": "typeclass.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "f9ee7145bf1d43ccf6dbd2147e7d9a4d938a9e70",
      "name": "typeobjs.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "2d8fd6763abbe32120848adf458ef1b52767e920",
      "name": "types.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "0c9394edeb43bca0564024352f4bc09fb33a6e7b",
      "name": "uint.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "82b7ef1e04acefc0f676d6023332d7668a5e3cb3",
      "name": "unifhint.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "a9b4c8233bd0476dc4bc8f2643bd1e169a573203",
      "name": "using_lean.md"
    },
    {
      "mode": 33188,
      "type": "blob",
      "id": "e1bcdeaeda96644b0748d0713beafd247edc2cad",
      "name": "whatIsLean.md"
    }
  ]
}