Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanEnvironment  |
| |
Examples
(2)
Scope
(1)
The available metadata properties:
In[1]:=
Information[env,"Properties"]
Out[1]=
{Constants,Kinds,Handle,Source,DeclOrder,Preamble}
How many constants of each kind:
In[2]:=
Information[env,"Kinds"]
Out[2]=
def6,theorem18,inductive1
Properties & Relations
(1)
 |
|
 |
|
Import the bundled environment: Its size and constant names: Index a constant by name to get a :
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]
 | LeanImport |
Out[1]=
LeanEnvironment
 |
|
In[2]:=
Length[env]
Out[2]=
25
In[3]:=
Keys[env]
Out[3]=
{Vec.head,id_proof,add_zero_term,fin_example,add_comm_proof,contrapositive,bor_false,eq_transport,add_succ_term,Vec.map,sigma_example,bnot_bnot,even_two,exists_succ,Vec.tail,and_comm_proof,add_assoc_proof,Vec,band_true,comp_proof,reverse_reverse,modus_ponens,nat_eq_decide,zero_add_proof,or_comm_proof}
In[4]:=
env["id_proof"]
Out[4]=
LeanTerm
|
|
""