Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExpr  |
|
| | ||||
▪
The result is a tree of CIC heads (, , , , , …) which render in Lean notation.
▪
Options: (the lake project), (modules to load), and (the expression-tree depth before a subtree becomes , default ).
"ProjectDir"
"Imports"
"Depth"
100
▪
queries a single constant; to load many at once into a use , after which gives the same tree.
env["name"]["Type"]
Examples
(2)
Basic Examples
(1)
Examples Initialization
The type of a Mathlib theorem as an expression tree (gated on a built checkout):
In[1]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];IfDirectoryQ[FileNameJoin[{mathlibDir,".lake","build"}]],
["And.comm","Imports"{"Mathlib.Logic.Basic"},"ProjectDir"mathlibDir],"Mathlib not built"
 | LeanExpr |
Out[1]=
{a:Prop}{b:Prop}
Iff
And
#1
#0
And
#0
#1
Properties & Relations
(1)
 |
|
 |
|
""