opaque Lean.neverExtractAttr : TagAttribute

Instructs the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, and that common subexpression elimination should not be performed.

Ordinarily, the Lean compiler identifies closed terms (without free variables) and extracts them to top-level definitions. This optimization can prevent unnecessary recomputation of values.

Preventing the extraction of closed terms is useful for declarations that have implicit effects that should be repeated.

@[export lean_has_never_extract_attribute]

def Lean.hasNeverExtractAttribute (env : Environment) (n : Name) : Bool

Equations

• Lean.hasNeverExtractAttribute env n = Lean.hasNeverExtractAttribute.visit env n

partial def Lean.hasNeverExtractAttribute.visit (env : Environment) (n : Name) : Bool