Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanToFunction  |
|
| | ||||
▪
is the lowering step that feeds to : it produces the uncompiled so you can inspect or modify it before compiling.
▪
Each Lean argument type becomes a slot with the corresponding Wolfram compiler type (/ to , and so on).
Nat
Int
"MachineInteger"
▪
Arithmetic, comparisons, Boolean connectives, and , and become their Wolfram Language counterparts; a call to any other function stays in the body, as a symbol of its name or, for a name such as that is not a symbol name, as the itself.
if
bif
max
min
"Nat.log2"
Examples
(4)
Basic Examples
(1)
A Lean definition, compiled from source:
In[1]:=
addEnv=
["def myAdd (x y : Nat) : Nat := x + y"]
 | LeanImportString |
Out[1]=
LeanEnvironment
 |
|
In[2]:=
 | LeanToFunction |
Out[2]=
Function[{Typed[x61,MachineInteger],Typed[y62,MachineInteger]},x61+y62]
Scope
(2)
Properties & Relations
(1)
 |
|
 |
|
""