Documentation

Lean.Compiler.LCNF.Simp.InlineCandidate

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.

Instances For

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

    Equations
      Instances For

        Return some info if e should be inlined.

        Equations
          Instances For