def Lean.Compiler.LCNF.hasLocalInst (type : Lean.Expr) : Bool

Return true if the arrow type contains an instance implicit argument.

Equations

• Lean.Compiler.LCNF.hasLocalInst (Lean.Expr.forallE binderName binderType b bi) = (Lean.BinderInfo.isInstImplicit bi || Lean.Compiler.LCNF.hasLocalInst b)
• Lean.Compiler.LCNF.hasLocalInst type = false

def Lean.Compiler.LCNF.Decl.isTemplateLike (decl : Lean.Compiler.LCNF.Decl) : Lean.CoreM Bool

Return true if decl is supposed to be inlined/specialized.

Equations

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

partial def Lean.Compiler.LCNF.Simp.findExpr (e : Lean.Expr) (skipMData : optParam Bool true) : Lean.Compiler.LCNF.CompilerM Lean.Expr

partial def Lean.Compiler.LCNF.Simp.findFunDecl? (e : Lean.Expr) : Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.FunDecl)