Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExprToType  |
|
| | ||||
▪
LeanExprToType
TypePi
LeanCompileTyped
▪
The resulting type object's methods (its form, unification, …) live in the Wolfram compiler's ; exercising them requires the forked compiler reached through the paclet's symlink.
"toString"
TypeFramework
compiler
Examples
(1)
Basic Examples
(1)
Examples Initialization
Translate a Lean arrow type to a compiler type object (shown without evaluating, since inspecting the object needs the forked compiler):
Nat->Nat
In[1]:=
 | LeanExprToType |
 | LeanForall |
 | LeanConst |
| LeanConst |
The call returns a / arrow type object over the leaf types map to; with the forked compiler loaded, its renders the Wolfram-side type and matches it against compiled signatures.
TypePi
Nat
"toString"
TypeUnify
 |
|
 |
|
""