@[export lean_add_extern]

def Lean.IR.addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit

Equations

• One or more equations did not get rendered due to their size.