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