loadTerms.lean
From the Lean 4 Zulip thread read term from file.
Building / Running
> lake build
[...]
> lake exe loadterms input
Hello, something
loadTerms
Testing dynamic term loading in Lean 4.
loadTermsFrom the Lean 4 Zulip thread read term from file.
> lake build
[...]
> lake exe loadterms input
Hello, something