Essential Lean 4 utilities and macros.
Embed file contents as string literals at compile time:
import Staple
-- Read a file relative to the current source file
def myTemplate : String := include_str% "templates/page.html"
-- Read a config file
def configJson : String := include_str% "../config.json"The file path is resolved relative to the source file containing the include_str% call.
- Lean 4.26.0
lake buildAdd to your lakefile.lean:
require staple from git "https://github.com/nathanial/staple" @ "v0.0.1"Then import in your Lean files:
import StapleMIT License - see LICENSE