In [12.4.3. @[extern] in the Interpreter](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=The-Lean-Language-Reference--Run-Time-Code--Foreign-Function-Interface--____LSQ_extern_RSQ_--in-the-Interpreter): > The Lean source repository contains an example of this usage in [tests/compiler/foreign](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/). `tests/compiler/foreign` no longer exists.
In 12.4.3. @[extern] in the Interpreter:
tests/compiler/foreignno longer exists.