Documentation

Lean.Compiler.Specialize

@[export lean_has_specialize_attribute]
@[export lean_has_nospecialize_attribute]
Instances For
    Equations
    Equations
    Equations
    Instances For
      Equations
      • { specInfo := m₁, cache := m₂ }.switch = { specInfo := m₁.switch, cache := m₂.switch }
      Instances For
        @[export lean_get_specialization_info]
        Equations
        Instances For
          @[export lean_get_cached_specialization]
          Equations
          Instances For