Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExprGraph  |
| | |||||
▪
The graph shows the constant's type and term as a tree of expression nodes. Where the in-process property of a works from an already-imported environment, runs the Lean toolchain out of process and reads back a DOT graph (via ).
"ExprGraph"
▪
Options include (bare files to load), / (a lake project and modules), (how many constant definitions to expand into, default ), and .
"Files"
.lean
"Imports"
"ProjectDir"
"ConstDepth"
1
"Depth"
▪
A subprocess call needs / on . Loading a large project (Mathlib) into the subprocess is slow; prefer bare for quick graphs.
lean
lake
PATH
"Files"
Examples
(2)
Basic Examples
(1)
Examples Initialization
The expression graph of a constant in the bundled examples file:
In[1]:=
ex=PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"];
["id_proof","Files"{ex}]
 | LeanExprGraph |
Out[1]=
Properties & Relations
(1)
 |
|
 |
|
""