{"repo":"tani/literate-lean","free":true,"listed":false,"github":"https://github.com/tani/literate-lean","clone":"git clone https://github.com/tani/literate-lean.git","description":"literate programming for lean4","language":"Lean","stars":10,"topics":["lean","lean4","literate-programming","markdown","public-domain"],"license":"Unlicense","category":"productivity","readme_excerpt":"LiterateLean for Lean 4 literate-lean is a small Lean 4 library for literate-programming style source files. It allows markdown-like prose in Lean files while executing explicit lean toml [[require]] name = \"LiterateLean\" git = \"https://github.com/tani/literate-lean.git\" rev = \"main\" lean import LiterateLean open scoped LiterateLean lean namespace Demo def success := \"This was evaluated!\" check success end Demo lean def answer : Nat := 42 lean module public import MyLibrary.Basic lean import MyLibrary eval answer bash lake build lake test lake env lean LiterateLean/Examples/Basic.lean Copyright Copyright (c) 2025-2026 Taniguchi Masaya. All Right Reserved.","default_branch":null,"files":null,"tree":[],"storefront":"/r/tani","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/tani/literate-lean/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}