feat: check new alwaysInline attribute

This commit is contained in:
Leonardo de Moura 2022-10-12 16:55:16 -07:00
parent 49a6f8c105
commit b9f174604d

View file

@ -62,6 +62,8 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do
-/
return false
let env ← getEnv
if hasAlwaysInlineAttribute env declName then return true
-- TODO: check inlining quota
if hasInlineAttribute env declName || inlineIfReduce then return true
unless hasNoInlineAttribute env declName do
if (← isSmall decl.value) then return true