Documentation

Lean.Util.FoldConsts

source
@[inline]
abbrev Lean.Expr.FoldConstsImpl.cacheSize:
USize
Equations
source
structure Lean.Expr.FoldConstsImpl.State:
Type
source
@[inline]
abbrev Lean.Expr.FoldConstsImpl.FoldM (α : Type) :
Type
Equations
source
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.
source
unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lean.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) :
Lean.Expr.FoldConstsImpl.FoldM α
Equations
source
unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lean.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) :
Lean.Expr.FoldConstsImpl.FoldM α
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Expr.FoldConstsImpl.initCache:
Lean.Expr.FoldConstsImpl.State
Equations
source
@[inline]
unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Name → α → α) :
α
Equations
source
@[implementedBy Lean.Expr.FoldConstsImpl.foldUnsafe]
opaque Lean.Expr.foldConsts {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Name → α → α) :
α

Apply f to every constant occurring in e once.

source
def Lean.Expr.getUsedConstants (e : Lean.Expr) :
Array Lean.Name
Equations
source
def Lean.getMaxHeight (env : Lean.Environment) (e : Lean.Expr) :
UInt32
Equations
  • One or more equations did not get rendered due to their size.