Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Lean 4 from the Wolfram Language
Wolfram`LeanLink`
LibraryLink
Importing and exporting
Environments and terms
Querying a loaded environment
the type of a constant as a symbolic expression tree
the proof or definition body of a constant
load a Lean environment handle for repeated queries
release a loaded environment handle
Expression heads (CIC)
a reference to a declared constant at given universe levels
function application
a bound variable by de Bruijn index
a free variable (local hypothesis or parameter)
a metavariable (unresolved placeholder)
a natural-number literal
a string literal
a structure-field projection
marks a constant with no body (axiom, opaque)
marks an expression cut off at the depth limit
Universe levels
the successor of a level
the maximum of two levels
the impredicative max (collapses to 0)
a universe metavariable
Interactive proofs
Transpiling Wolfram proofs
Compiling Lean to native code
LeanCompileTyped
LeanExprToType
Out-of-process project queries
expression graph for a constant, computed by a Lean subprocess
call / dependency graph for a constant, via subprocess
list a project's theorems via subprocess
""