Documentation
Lean.Compiler.IR.UnboxResult
Google site search
Lean.Compiler.IR.UnboxResult
source
Imports
Init
Lean.Data.Format
Lean.Compiler.IR.Basic
Imported by
Lean.IR.UnboxResult.unboxAttr
Lean.IR.UnboxResult.hasUnboxAttr
source
opaque
Lean.IR.UnboxResult.unboxAttr
:
Lean.TagAttribute
source
def
Lean.IR.UnboxResult.hasUnboxAttr
(env :
Lean.Environment
)
(n :
Lean.Name
)
:
Bool
Equations
Lean.IR.UnboxResult.hasUnboxAttr
env
n
=
Lean.TagAttribute.hasTag
Lean.IR.UnboxResult.unboxAttr
env
n