Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanTerm  |
| | |
| |
Examples
(2)
Scope
(1)
In[1]:=
env["modus_ponens"]["Parameters"]//Dataset
Out[1]=
|
The expression tree as a graph:
In[2]:=
env["id_proof"]["ExprGraph"]
Out[2]=
Properties & Relations
(1)
 |
|
 |
|
A constant from an imported environment: Its type as Lean source, and its proof body: The type as a symbolic tree (rendered in Lean notation by the boxes):
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];env["id_proof"]
 | LeanImport |
Out[1]=
LeanTerm
 |
|
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
""