Basic Examples

Import a focused mathlib module:
In[1]:=
env=LeanImport"Mathlib.Data.Nat.Choose.Basic","ProjectDir"->
MathlibInstallation
[]["Directory"]
Out[1]=
LeanEnvironment
Constants: 140255
Kinds: 59439 def4214 constructor71138 theorem2780 opaque2668 inductive12 axiom4 quot
This object cannot be used as input.

Compute an exact binomial coefficient:
In[2]:=
LeanEvaluate[env["Nat.choose"],10,4]
Out[2]=
LeanEvaluateLeanTerm
Kind: def
Name: Nat.choose
,10,4
Read a theorem's type:
In[3]:=
env["Nat.add_comm"]["TypeForm"]
Out[3]=
∀ (n m : ℕ), n + m = m + n
Release the environment:
In[4]:=
LeanFreeEnvironment[env]
Out[4]=
LeanFreeEnvironmentLeanEnvironment
Constants: 140255
Kinds: 59439 def4214 constructor71138 theorem2780 opaque2668 inductive12 axiom4 quot
This object cannot be used as input.
