Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanLam  |
|
| | ||||
▪
binder is the bracket kind, as for : , , , .
"default"
"implicit"
"instImplicit"
"strictImplicit"
▪
Where is the function type, is the function value. It renders as Lean , with referring back to the binder.
fun(x:T)=>body
Examples
(2)
Basic Examples
(1)
Examples Initialization
The identity function on naturals, :
fun(x:Nat)=>x
In[1]:=
 | LeanLam |
 | LeanConst |
| LeanBVar |
Out[1]=
fun(x:)
Nat
#0
Properties & Relations
(1)
 |
|
 |
|
""