- specialize : SpecializeAttributeKind
- nospecialize : SpecializeAttributeKind
Instances For
Marks a definition to never be specialized during code generation.
Marks a definition to always be specialized during code generation.
Specialization is an optimization in the code generator for generating variants of a function that
are specialized to specific parameter values. This is in particular useful for functions that take
other functions as parameters: Usually when passing functions as parameters, a closure needs to be
allocated that will then be called. Using @[specialize]
prevents both of these operations by
using the provided function directly in the specialization of the inner function.
@[specialize]
can take additional arguments for the parameter names or indices (starting at 1) of
the parameters that should be specialized. By default, instance and function parameters are
specialized.
Equations
- Lean.Compiler.getSpecializationArgs? env declName = Lean.Compiler.specializeAttr.getParam? env declName
Instances For
Equations
- Lean.Compiler.hasSpecializeAttribute env declName = (Lean.Compiler.getSpecializationArgs? env declName).isSome
Instances For
Equations
- Lean.Compiler.hasNospecializeAttribute env declName = Lean.Compiler.nospecializeAttr.hasTag env declName
Instances For
- fixed : SpecArgKind
- fixedNeutral : SpecArgKind
- fixedHO : SpecArgKind
- fixedInst : SpecArgKind
- other : SpecArgKind
Instances For
Equations
- argKinds : List SpecArgKind
Instances For
Equations
Equations
Instances For
Equations
Instances For
Equations
- Lean.Compiler.getSpecializationInfo env fn = (Lean.Compiler.specExtension.getState env).specInfo.find? fn