- specialize: Lean.Compiler.SpecializeAttributeKind
- nospecialize: Lean.Compiler.SpecializeAttributeKind
Instances For
Instances For
Instances For
Instances For
@[export lean_has_specialize_attribute]
@[export lean_has_nospecialize_attribute]
- fixed: Lean.Compiler.SpecArgKind
- fixedNeutral: Lean.Compiler.SpecArgKind
- fixedHO: Lean.Compiler.SpecArgKind
- fixedInst: Lean.Compiler.SpecArgKind
- other: Lean.Compiler.SpecArgKind
Instances For
- argKinds : List Lean.Compiler.SpecArgKind
Instances For
- specInfo : Lean.SMap Lake.Name Lean.Compiler.SpecInfo
Instances For
- info: Lake.Name → Lean.Compiler.SpecInfo → Lean.Compiler.SpecEntry
- cache: Lean.Expr → Lake.Name → Lean.Compiler.SpecEntry
Instances For
Instances For
Instances For
@[export lean_add_specialization_info]
def
Lean.Compiler.addSpecializationInfo
(env : Lean.Environment)
(fn : Lake.Name)
(info : Lean.Compiler.SpecInfo)
:
Instances For
@[export lean_get_specialization_info]
Instances For
@[export lean_cache_specialization]
Instances For
@[export lean_get_cached_specialization]