← Copula mathematical handbook

opaque Lean.IR.UnboxResult.unboxAttr : TagAttribute

Tags types that the compiler should unbox if they occur in result values.

This attribute currently has no effect.

def Lean.IR.UnboxResult.hasUnboxAttr (env : Environment) (n : Name) : Bool

Equations

• Lean.IR.UnboxResult.hasUnboxAttr env n = Lean.IR.UnboxResult.unboxAttr.hasTag env n