Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanLoadEnvironment  |
|
| | ||||
▪
searchPath lists every directory the modules' compiled files come from, separated by : the project's own build directory (for a lake project, ), each dependency's, and the Lean toolchain's , which holds . assembles this path for you from .
.olean
":"
<project>/.lake/build/lib/lean
lib/lean
Init
"ProjectDir"
▪
The returned handle is a positive integer naming a native environment held open in the Lean runtime. A failed load returns .
0
▪
Use the handle for many / style queries against one loaded environment without reloading it each time, then release it with .
▪
Most workflows use instead, which loads, queries, and wraps constants in one step. is the lower-level door for repeated queries where holding the environment open matters.
Examples
(2)
Basic Examples
(1)
Load the core module from the Lean toolchain into an environment handle, then free it:
Init
In[1]:=
toolchainLib=FileNameJoin[{$HomeDirectory,".elan","toolchains","leanprover--lean4---v4.35.0","lib","lean"}];IfDirectoryQ[toolchainLib],handle=
[{"Init"},toolchainLib];result=handle>0;
[handle];result,"Lean toolchain not installed"
 | LeanLoadEnvironment |
 | LeanFreeEnvironment |
Out[1]=
True
Possible Issues
(1)
 |
|
 |
|
""