Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanLoadEnvironment  |
|
| | ||||
▪
searchPath is the directory holding the compiled files (for a lake project, typically ). The returned handle is an integer naming a native environment held open in the Lean runtime.
.olean
<project>/.lake/build/lib/lean
▪
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)
Examples Initialization
Load a Mathlib module into an environment handle, then free it (gated on a built checkout):
In[1]:=
leanLib=FileNameJoin[{$HomeDirectory,"src","mathlib4",".lake","build","lib","lean"}];IfDirectoryQ[leanLib],handle=
[{"Mathlib.Logic.Basic"},leanLib];result=IntegerQ[handle];
[handle];result,"Mathlib not built"
 | LeanLoadEnvironment |
 | LeanFreeEnvironment |
Out[1]=
True
Possible Issues
(1)
 |
|
 |
|
""