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

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

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

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

• fType : Lean.Expr
• args : Array Lean.Compiler.LCNF.Arg
• ifReduce : Bool

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

• recursive : Bool

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

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

• x.arity = match x with | { isLocal := isLocal, params := params, value := value, fType := fType, args := args, ifReduce := ifReduce, recursive := recursive } => params.size

def Lean.Compiler.LCNF.Simp.inlineCandidate? (e : Lean.Compiler.LCNF.LetValue) : 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.