Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanFreeEnvironment  |
|
| | ||||
▪
handle is the integer returned by . After freeing, the handle is no longer valid for queries.
▪
Examples
(2)
Basic Examples
(1)
Examples Initialization
Load and immediately free an environment (gated on a built mathlib4 checkout):
In[1]:=
leanLib=FileNameJoin[{$HomeDirectory,"src","mathlib4",".lake","build","lib","lean"}];IfDirectoryQ[leanLib],handle=
[{"Mathlib.Logic.Basic"},leanLib];
[handle],"Mathlib not built"
 | LeanLoadEnvironment |
 | LeanFreeEnvironment |
Properties & Relations
(1)
 |
|
 |
|
""