Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanTactic  |
|
| | ||||
|
| | ||||
|
| | ||||
| | |||||
▪
A tactic runs directly in Lean's meta-programming monad, without Lean's tactic parser, which an environment loaded from compiled modules lacks. These tactics work: with or without names, , with a constant or hypothesis applied to others (), with a constant or hypothesis, , , and . Any other tactic, and terms beyond names applied to names, such as or , give with a message.
intro
intros
exact
exacthPQhP
apply
assumption
rfl
constructor
trivial
h.1
⟨a,b⟩
LeanTactic::err
▪
The string form writes the tactic as in Lean. The structured form names a tactic and supplies its arguments as Wolfram values: , .
▪
A list groups tactics into a sequence applied left to right, equivalent to applying each in turn.
▪
Application is a pure transformation of proof states: each step returns a new rather than mutating the old one.
Examples
(2)
Basic Examples
(1)
A tactic as a value:
In[1]:=
 | LeanTactic |
Out[1]=
intro P
The example environment bundled with the paclet:
In[2]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]
 | LeanImport |
Out[2]=
LeanEnvironment
 |
|
Its identity theorem, opened as a proof state:
In[3]:=
s0=
[env["id_proof"]]
| LeanState |
Out[3]=
1 goal | ||
|
Apply a sequence to the proof state:
In[4]:=
s1=
[{"intro P","intro h","exact h"}][s0]
 | LeanTactic |
Out[4]=
✓ No goals
It closes the goal:
In[5]:=
s1["Complete"]
Out[5]=
True
Scope
(1)
 |
|
""