Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanCompile  |
| | |||||
|
| | ||||
▪
The Lean definition's argument and result types are mapped to Wolfram compiler types - and to , to , to , to - and the body is lowered through .
Nat
Int
"MachineInteger"
Bool
"Boolean"
Float
"Real64"
String
"String"
▪
Only computational definitions compile; propositions and theorems are skipped by the environment form.
▪
The non-dependent path runs against the stock Wolfram compiler. The dependent-type path ( sizes carried in a signature) needs a forked compiler; see and [Possible Issues].
Vector
TypePi
LeanCompileTyped
Examples
(3)
Basic Examples
(1)
Examples Initialization
Compile a Lean definition to a native function and run it:
In[1]:=
addEnv=
["def myAdd (x y : Nat) : Nat := x + y"];cf=
[addEnv["myAdd"]]
 | LeanImportString |
 | LeanCompile |
Out[1]=
CompiledCodeFunction
 |
|
In[2]:=
cf[3,4]
Out[2]=
7
Scope
(1)
Possible Issues
(1)
 |
|
 |
|
""