Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanListTheorems  |
|
| | ||||
▪
Options: , / , and (keep only names containing the substring).
"Files"
"Imports"
"ProjectDir"
"Filter"
▪
Loading a file pulls in its full transitive environment - including the Lean prelude - so an unfiltered call returns tens of thousands of rows. Always pass a .
"Filter"
Examples
(2)
Basic Examples
(1)
Examples Initialization
List the theorems in the bundled examples file, narrowed by name:
In[1]:=
ex=PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"];
["Files"{ex},"Filter""modus_ponens"]
 | LeanListTheorems |
Out[1]=
|
Possible Issues
(1)
 |
|
 |
|
""