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

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

• isLocal : Bool
• params : Array Param
• value : Code

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

• fType : Expr
• args : Array 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 : InlineCandidateInfo → Nat

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

Equations

• { isLocal := isLocal, params := params, value := value, fType := fType, args := args, ifReduce := ifReduce, recursive := recursive }.arity = params.size

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

Return some info if e should be inlined.

Equations

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