Wolfram Language
Paclet Repository
Community-contributed installable additions to the Wolfram Language
Primary Navigation
Categories
Cloud & Deployment
Core Language & Structure
Data Manipulation & Analysis
Engineering Data & Computation
External Interfaces & Connections
Financial Data & Computation
Geographic Data & Computation
Geometry
Graphs & Networks
Higher Mathematical Computation
Images
Knowledge Representation & Natural Language
Machine Learning
Notebook Documents & Presentation
Scientific and Medical Data & Computation
Social, Cultural & Linguistic Data
Strings & Text
Symbolic & Numeric Computation
System Operation & Setup
Time-Related Computation
User Interface Construction
Visualization & Graphics
Random Paclet
Alphabetical List
Using Paclets
Create a Paclet
Get Started
Download Definition Notebook
Learn More about
Wolfram Language
LeanLink
Guides
Lean 4 from the Wolfram Language
Tech Notes
Exploring Mathlib with LeanLink
An Import Graph for Mathlib
Getting Started with LeanLink
Symbols
ImportDOT
LeanApp
LeanBVar
LeanCallGraph
LeanCompile
LeanCompileTyped
LeanConstantInfo
LeanConstant
LeanConst
LeanEnvironment
LeanExport
LeanExportString
LeanExprGraph
LeanExpr
LeanExprToType
LeanForall
LeanFreeEnvironment
LeanFVar
LeanGoal
LeanImport
LeanImportString
LeanLam
LeanLet
LeanLevelIMax
LeanLevelMax
LeanLevelMVar
LeanLevelParam
LeanLevelSucc
LeanLevelZero
LeanListConstants
LeanListTheorems
LeanLitNat
LeanLitStr
LeanLoadEnvironment
LeanMVar
LeanNoValue
LeanProj
LeanSort
LeanState
LeanTactic
LeanTerm
LeanToFunction
LeanTruncated
LeanValue
ProofToLean
Wolfram`LeanLink`
L
e
a
n
L
i
t
N
a
t
L
e
a
n
L
i
t
N
a
t
[
n
]
r
e
p
r
e
s
e
n
t
s
a
L
e
a
n
n
a
t
u
r
a
l
-
n
u
m
b
e
r
l
i
t
e
r
a
l
n
.
D
e
t
a
i
l
s
a
n
d
O
p
t
i
o
n
s
▪
n
is a non-negative integer. It renders as the number itself.
Examples
(
1
)
Basic Examples
(
1
)
Examples Initialization
A natural-number literal:
I
n
[
1
]
:
=
L
e
a
n
L
i
t
N
a
t
[
4
2
]
O
u
t
[
1
]
=
4
2
As the argument of an application,
N
a
t
.
s
u
c
c
4
2
:
I
n
[
2
]
:
=
L
e
a
n
A
p
p
L
e
a
n
C
o
n
s
t
[
"
N
a
t
.
s
u
c
c
"
]
,
L
e
a
n
L
i
t
N
a
t
[
4
2
]
O
u
t
[
2
]
=
N
a
t
.
s
u
c
c
4
2
S
e
e
A
l
s
o
L
e
a
n
L
i
t
S
t
r
▪
L
e
a
n
C
o
n
s
t
▪
L
e
a
n
A
p
p
R
e
l
a
t
e
d
G
u
i
d
e
s
▪
L
e
a
n
L
i
n
k
"
"
