Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanListTheorems  |
| lists a project's theorems, returning a with "Kind" "Name" | |
Examples
(1)
Possible Issues
(1)
Without a , returns the entire transitive environment (the prelude alone is tens of thousands of declarations). Narrow with , or use the from with a filter for a typed, queryable result.
"Filter"
"Filter"
 |
|
 |
|
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]=
|
""