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"
▪
Arithmetic (, , , , , ), comparisons, and , the connectives , , and , and , and , decimal literals, and the conversions from to and to become their Wolfram Language counterparts, and compute as Lean's do on and : stops at 0 on , dividing by 0 gives 0, and is 1.
+
-
*
/
%
^
≠
&&
||
!
xor
if
bif
max
min
Nat
Int
Float
Nat
Int
a-b
Nat
0^0
▪
A call to any other function, another definition included, stays in the body as it is, and the definition does not compile.
▪
Only computational definitions compile; propositions and theorems are skipped by the environment form.
▪
A dependent type, such as , where the size appears in the type, has no compiler type, so a definition of that type does not compile.
VectorIntn
n
Examples
(3)
Basic Examples
(1)
A Lean definition, compiled from source:
In[1]:=
addEnv=
["def myAdd (x y : Nat) : Nat := x + y"]
 | LeanImportString |
Out[1]=
LeanEnvironment
 |
|
Compile a Lean definition to a native function:
In[2]:=
cf=
[addEnv["myAdd"]]
| LeanCompile |
Out[2]=
CompiledCodeFunction
 |
|
Run it:
In[3]:=
cf[3,4]
Out[3]=
7
Scope
(2)
 |
|
 |
|
""