Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanImport  |
| | |||||
|
| | ||||
▪
The result is a - a typed wrapper over . Index it by constant name, or query it with , , and .
▪
A module argument () is resolved inside a Lean project; a file argument is a path to a source file (such as the bundled ).
"Mathlib.Algebra.Group.Basic"
.lean
Examples.lean
▪
The following options are accepted:
Option | Default | Description | |
"ProjectDir" | Automatic | the lake project the module is resolved in | |
"Imports" | {} | extra modules to load alongside the target | |
"Filter" | "" | keep only constants whose name contains this substring | |
"IncludeInternal" | False | include compiler-internal / private declarations |
▪
Importing a module requires that project to be built (). An unbuilt or missing module yields an empty environment, not an error.
lakebuild
Examples
(3)
Basic Examples
(1)
Examples Initialization
Import the bundled example environment from its file path:
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]
 | LeanImport |
Out[1]=
LeanEnvironment
 |
|
How many constants it holds:
In[2]:=
Length[env]
Out[2]=
25
The constant names:
In[3]:=
Keys[env]
Out[3]=
{id_proof,add_zero_term,bor_false,eq_transport,Vec.map,sigma_example,even_two,exists_succ,Vec,band_true,comp_proof,reverse_reverse,zero_add_proof,Vec.head,fin_example,add_comm_proof,contrapositive,add_succ_term,bnot_bnot,Vec.tail,and_comm_proof,add_assoc_proof,modus_ponens,nat_eq_decide,or_comm_proof}
In[4]:=
env["id_proof"]["TypeForm"]
Out[4]=
∀ (P : Prop) (a : P), P
Scope
(1)
Possible Issues
(1)
 |
|
 |
|
""