- specialize : SpecializeAttributeKind
- nospecialize : SpecializeAttributeKind
Instances For
@[export lean_has_specialize_attribute]
@[export lean_has_nospecialize_attribute]
- fixed : SpecArgKind
- fixedNeutral : SpecArgKind
- fixedHO : SpecArgKind
- fixedInst : SpecArgKind
- other : SpecArgKind
Instances For
Equations
- argKinds : List SpecArgKind
Instances For
Equations
- Lean.Compiler.instInhabitedSpecInfo = { default := { mutualDecls := default, argKinds := default } }
Equations
- Lean.Compiler.instInhabitedSpecState = { default := { specInfo := default, cache := default } }
Equations
Equations
Instances For
Equations
- { specInfo := m₁, cache := m₂ }.switch = { specInfo := m₁.switch, cache := m₂.switch }
Instances For
@[export lean_add_specialization_info]
Equations
Instances For
@[export lean_get_specialization_info]
Equations
Instances For
@[export lean_cache_specialization]
Equations
Instances For
@[export lean_get_cached_specialization]