Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanTerm  |
|
| | ||||
|
| | ||||
▪
Property | Result | |
"Type" "Term" | the type / body as a symbolic expression tree | |
"TypeForm" "TermForm" | the type / body pretty-printed as Lean source | |
"Parameters" | the binder chain (name, type, binder kind) as rows | |
"TypeRefs" "TermRefs" | constants the type / body refers to | |
"ExprGraph" "CallGraph" | ||
"Name" "Kind" | the constant's name / declaration kind |
▪
The expression tree is built from the CIC heads , , , , , , , … which carry box formatting, so a displays in Lean notation rather than as raw heads.
"Type"
Examples
(3)
Basic Examples
(1)
Examples Initialization
A constant from an imported environment:
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];env["id_proof"]
 | LeanImport |
Out[1]=
LeanTerm
 |
|
Its type as Lean source, and its proof body:
In[2]:=
env["id_proof"]["TypeForm"]
Out[2]=
∀ (P : Prop) (a : P), P
In[3]:=
env["id_proof"]["TermForm"]
Out[3]=
fun x hp => hp
In[4]:=
env["id_proof"]["Type"]
Out[4]=
(P:Prop)(a:)
#0
#1
Scope
(1)
Properties & Relations
(1)
 |
|
 |
|
""