Wolfram/LeanLink | Paclet Repository

Wolfram`LeanLink`

LeanEnvironment

LeanEnvironment [assoc]
	holds a collection of named Lean constants, where assoc maps each name to a LeanTerm .

Details and Options

▪

A

is produced by

,

, or

- you rarely build one by hand.

▪

Index it by constant name to get a

LeanTerm

:

env["mul_comm"]

. It also supports

,

,

,

, and

(which returns the underlying

Association

).

▪

Information

[env,prop]

exposes environment metadata. Properties:

"Constants"

(the names),

"Kinds"

(a count by declaration kind),

"Handle"

(the native environment id),

"Source"

,

"DeclOrder"

,

"Preamble"

.

Examples

(3)

Basic Examples

(1)

Examples Initialization

Import the bundled environment:

In[1]:=

env=

LeanImport

[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]

Out[1]=

LeanEnvironment

Constants: 25

Kinds: 18 theorem6 def1 inductive



Its size and constant names:

In[2]:=

Length[env]

Out[2]=

25

In[3]:=

Keys[env]

Out[3]=

{id_proof,add_zero_term,bor_false,eq_transport,Vec.map,sigma_example,even_two,exists_succ,Vec,band_true,comp_proof,reverse_reverse,zero_add_proof,Vec.head,fin_example,add_comm_proof,contrapositive,add_succ_term,bnot_bnot,Vec.tail,and_comm_proof,add_assoc_proof,modus_ponens,nat_eq_decide,or_comm_proof}

Index a constant by name to get a

LeanTerm

:

In[4]:=

env["id_proof"]

Out[4]=

LeanTerm