Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanState  |
▪
Advance the state by applying a : returns the new . A proof is finished when is .
LeanTactic[tac][state]
"Complete"
True
▪
Opening a state from a fully-proved theorem still presents the statement as a goal to re-derive interactively; tactics operate on the goal stack the same way Lean's tactic mode does.
Examples
(3)
Basic Examples
(1)
Examples Initialization
Open a theorem as a goal:
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]];s0=
[env["id_proof"]]
 | LeanImport |
 | LeanState |
Out[1]=
1 goal | ||
|
How many goals remain, and whether it is finished:
In[2]:=
s0["GoalCount"]
Out[2]=
1
In[3]:=
s0["Complete"]
Out[3]=
False
The first goal's target:
In[4]:=
s0["Goals"]〚1〛["Target"]
Out[4]=
∀ (P : Prop), P → P
Scope
(1)
Possible Issues
(1)
 |
|
 |
|
""