Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanConstant  |
| |
▪
is the low-level record returns and collects. The higher-level wraps the same data with the property interface (, , …).
"TypeForm"
"ExprGraph"
▪
kind is a string such as , , , , or . type and term are CIC expression trees (or for a constant with no body).
"theorem"
"def"
"inductive"
"constructor"
"axiom"
Examples
(0)
 |
|
 |
|
The raw record of a Mathlib theorem (gated on a built checkout): The name and kind are the first two parts:
In[1]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];IfDirectoryQ[FileNameJoin[{mathlibDir,".lake","build"}]],
["And.comm","Imports"{"Mathlib.Logic.Basic"},"ProjectDir"mathlibDir],"Mathlib not built"
 | LeanConstantInfo |
Out[1]=
LeanConstant[And.comm,theorem,{a:Prop}{b:Prop},fun{a:Prop}fun{b:Prop}]
Iff
And
#1
#0
And
#0
#1
Iff.intro
And
#1
#0
And
#0
#1
And.symm
#1
#0
And.symm
#0
#1
In[2]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];IfDirectoryQ[FileNameJoin[{mathlibDir,".lake","build"}]],info=
["And.comm","Imports"{"Mathlib.Logic.Basic"},"ProjectDir"mathlibDir];{info〚1〛,info〚2〛},"Mathlib not built"
 | LeanConstantInfo |
Out[2]=
{And.comm,theorem}
""