@[inline, reducible]

abbrev Lean.Expr.FoldConstsImpl.cacheSize : USize

Equations

• Lean.Expr.FoldConstsImpl.cacheSize = 8192 - 1

structure Lean.Expr.FoldConstsImpl.State : Type

• visitedTerms : Array Lean.Expr
• visitedConsts : Lean.NameHashSet

@[inline, reducible]

abbrev Lean.Expr.FoldConstsImpl.FoldM (α : Type) : Type

Equations

• Lean.Expr.FoldConstsImpl.FoldM = StateM Lean.Expr.FoldConstsImpl.State

unsafe def Lean.Expr.FoldConstsImpl.visited (e : Lean.Expr) (size : USize) : Lean.Expr.FoldConstsImpl.FoldM Bool

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lake.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) : Lean.Expr.FoldConstsImpl.FoldM α

Equations

• Lean.Expr.FoldConstsImpl.fold f size e acc = Lean.Expr.FoldConstsImpl.fold.visit f size e acc

unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lake.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) : Lean.Expr.FoldConstsImpl.FoldM α

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Expr.FoldConstsImpl.initCache : Lean.Expr.FoldConstsImpl.State

Equations

• One or more equations did not get rendered due to their size.

@[inline]

unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Lean.Expr) (init : α) (f : Lake.Name → α → α) : α

Equations

• Lean.Expr.FoldConstsImpl.foldUnsafe e init f = StateT.run' (Lean.Expr.FoldConstsImpl.fold f Lean.Expr.FoldConstsImpl.cacheSize e init) Lean.Expr.FoldConstsImpl.initCache

@[implemented_by Lean.Expr.FoldConstsImpl.foldUnsafe]

opaque Lean.Expr.foldConsts {α : Type} (e : Lean.Expr) (init : α) (f : Lake.Name → α → α) : α

Apply f to every constant occurring in e once.

def Lean.Expr.getUsedConstants (e : Lean.Expr) : Array Lake.Name

Equations

• Lean.Expr.getUsedConstants e = Lean.Expr.foldConsts e #[] fun (c : Lake.Name) (cs : Array Lake.Name) => Array.push cs c

def Lean.Expr.getUsedConstantsAsSet (e : Lean.Expr) : Lean.NameSet

Like Expr.getUsedConstants, but produce a NameSet.

Equations

• Lean.Expr.getUsedConstantsAsSet e = Lean.Expr.foldConsts e ∅ fun (c : Lake.Name) (cs : Lean.NameSet) => Lean.NameSet.insert cs c

def Lean.ConstantInfo.getUsedConstantsAsSet (c : Lean.ConstantInfo) : Lean.NameSet

Return all names appearing in the type or value of a ConstantInfo.

Equations

• One or more equations did not get rendered due to their size.

def Lean.getMaxHeight (env : Lean.Environment) (e : Lean.Expr) : UInt32

Equations

• One or more equations did not get rendered due to their size.