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, with its packages and path dependencies | |
"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 (). A module with no compiled file in the project's search path fails: returns with a message that names it.
lakebuild
.olean
▪
A file can other files of its folder, or of the Lake project around it: they are compiled first, in import order, so finds next to the file and finds . A GitHub URL import does the same with the files it downloads.
import
.lean
importB
B.lean
importSub.C
Sub/C.lean
Examples
(4)
Basic Examples
(1)
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]=
32
The constant names:
In[3]:=
Keys[env]
Out[3]=
{id_proof,Vec.head,band_true,add_assoc_proof,comp_proof,even_two,Vec.ctorElimType,bor_false,zero_add_proof,bnot_bnot,Vec.cons,Vec,eq_transport,add_comm_proof,nat_eq_decide,contrapositive,Vec.nil,reverse_reverse,Vec.cons.elim,Vec.map,or_comm_proof,fin_example,exists_succ,sigma_example,add_zero_term,add_succ_term,Vec.nil.elim,modus_ponens,and_comm_proof,Vec.ctorElim,Vec.tail,Vec.ctorIdx}
In[4]:=
env["id_proof"]["TypeForm"]
Out[4]=
∀ (P : Prop), P → P
Scope
(1)
Possible Issues
(2)
 |
|
 |
|
""