structure Lean.Compiler.LCNF.Simp.InlineCandidateInfo : Type

• isLocal : Bool
• params : Array Lean.Compiler.LCNF.Param

• Value (lambda expression) of the function to be inlined.

  value : Lean.Compiler.LCNF.Code
• f : Lean.Expr
• args : Array Lean.Expr

• ifReduce = true if the declaration being inlined was tagged with inlineIfReduce.

  ifReduce : Bool

• recursive = true if the declaration being inline is in a mutually recursive block.

  recursive : Bool

Result of inlineCandidate?. It contains information for inlining local and global functions.

def Lean.Compiler.LCNF.Simp.InlineCandidateInfo.arity : Lean.Compiler.LCNF.Simp.InlineCandidateInfo → Nat

The arity (aka number of parameters) of the function to be inlined.

Equations

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

def Lean.Compiler.LCNF.Simp.inlineCandidate? (e : Lean.Expr) : Lean.Compiler.LCNF.Simp.SimpM (Option Lean.Compiler.LCNF.Simp.InlineCandidateInfo)

Return some info if e should be inlined.

Equations

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