Wolfram/LeanLink | Paclet Repository

Wolfram`LeanLink`

LeanTerm

LeanTerm [assoc]
	represents one Lean constant - its name, kind, type, and body - as returned by indexing a LeanEnvironment .

LeanTerm [expr,env]
	wraps a hand-built expression tree expr, bound to environment env so it can be type-checked.

Details and Options

▪

A

renders as a summary box (icon, name, kind). Query it with properties via

term["prop"]

:

	Property	Result
	"Type" / "Term"	the type / body as a symbolic expression tree
	"TypeForm"	the type as #check prints it, from Lean's own printer; term["TypeForm","Open"->{ns,...}] prints names under those namespaces unqualified
	"TermForm"	the body pretty-printed as Lean source
	"Parameters"	the binder chain (name, type, binder kind) as rows
	"TypeRefs" / "TermRefs"	constants the type / body refers to
	"Axioms"	the axioms the constant depends on, as #printaxioms reports them; like it, this trusts that every declaration passed the kernel (see Possible Issues)
	"KernelCheck"	the module that declares the constant, replayed through Lean's kernel as leanchecker does: a Success , or a Failure with the kernel's message
	"Module"	the module that declares the constant
	"Source"	the declaration's source text
	"ExprGraph" / "CallGraph"	a Graph of the expression tree / dependencies (a display graph: it omits auxiliary declarations, so use "Axioms" , not "CallGraph" , to audit axioms)
	"Name" / "Kind"	the constant's name / declaration kind

▪

The expression tree is built from the CIC heads

,

,

,

,

,

,

, … which carry box formatting, so a

"Type"

displays in Lean notation rather than as raw heads.

Examples

(4)

Basic Examples

(1)

The example environment bundled with the paclet:

In[1]:=

env=

LeanImport

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

Out[1]=

LeanEnvironment

Constants: 32

Kinds: 18 theorem11 def2 constructor1 inductive



A constant from an imported environment:

In[2]:=

env["id_proof"]

Out[2]=

LeanTerm

Kind: theorem

Name: id_proof



Its type as Lean source:

In[3]:=

env["id_proof"]["TypeForm"]

Out[3]=

∀ (P : Prop), P → P

Its proof body:

In[4]:=

env["id_proof"]["TermForm"]

Out[4]=

fun x hp => hp

The type as a symbolic tree (rendered in Lean notation by the

boxes):

In[5]:=

env["id_proof"]["Type"]

Out[5]=

(P:Prop)(a:

#0

)

#1

Scope

(1)



Properties & Relations

(1)



Possible Issues

(1)



SeeAlso

LeanEnvironment

▪

▪

▪

▪

RelatedGuides

▪

Lean 4 from the Wolfram Language

""