Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanImportString  |
| | |||||
|
| | ||||
▪
src is ordinary Lean 4 source: any mix of , , , , and so on. Each top-level declaration becomes one in the result.
def
theorem
inductive
structure
▪
The string is compiled by the of LeanLink's pinned toolchain and loaded into the embedded runtime. A type error in src returns with a message carrying Lean's diagnostic, as would report it.
lean
LeanImport::err
lakebuild
▪
With , src can the modules of the built Lake project in dir, of its packages, and of its path dependencies ( in the lakefile). A theorem proved against the project's definitions is then a kernel-checked claim about them.
"ProjectDir"*dir*
import
path="../x"
bydecide
▪
Declarations inside a are kept under their full names.
namespace
▪
A list of sources is one source, joined with newlines: an line, a few declarations and generated source go in as they are, with no string joining.
import
▪
Use for ad-hoc definitions and round-trips; use to pull constants from a compiled module such as Mathlib.
Examples
(4)
Basic Examples
(1)
Compile a single theorem:
In[1]:=
imported=
["theorem myT : Nat.succ 0 = 1 := rfl"]
 | LeanImportString |
Out[1]=
LeanEnvironment
 |
|
Read back its type:
In[2]:=
imported["myT"]["TypeForm"]
Out[2]=
Nat.succ 0 = 1
Scope
(1)
Properties & Relations
(1)
Possible Issues
(1)
 |
|
 |
|
""