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 elaborated by the embedded Lean runtime, so a type error in src surfaces as a the same way would report it.
lakebuild
▪
Use for ad-hoc definitions and round-trips; use to pull constants from a compiled module such as Mathlib.
Examples
(3)
Basic Examples
(1)
Examples Initialization
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)
 |
|
 |
|
""