@[extern lean_load_dynlib]

opaque Lean.loadDynlib (path : Lake.FilePath) : IO Unit

Dynamically loads a shared library so that its symbols can be used by the Lean interpreter (e.g., for interpreting @[extern] declarations). Equivalent to passing --load-dynlib=lib to lean.

Note that Lean never unloads libraries.