Standard TLA⁺ modules (Sequences, TLC, Naturals, FiniteSets, …) — a hardcoded table of already-checked Modules, not bundled .tla stub files: standard-library operators (Len, Head, Append, …) get replaced by backend-native implementations at code-generation time regardless of what their "definition" says.

Kept as full Modules (not a bare declaration list) so the Γ-merge step in Driver/Modules.lean's compileModule treats a builtin hit and a real resolved dependency identically. Still subject to the same ambiguity rule as any other candidate source: a user's own module of the same name is not silently shadowed by a builtin, or vice versa.

def builtinModules : Std.HashMap String TypedModule

The table itself (doc above). «extends» mirrors each real module's own top-of-file dependency list (EXTENDS/LOCAL INSTANCE alike — LOCAL only means "not re-exported" in real TLA⁺, not "not a dependency", and resolveModule/compileModule don't distinguish the two anyway), so a module that only EXTENDS Sequences/Integers/FiniteSets/Bags still transitively sees everything that real module itself imports. RealTime/Reals are out of scope entirely (never ported). Fugue is the one entry with no real counterpart — this compiler's own module; it EXTENDS Naturals, since a downcast's 1 .. n domain is unwritable without it, so EXTENDS Fugue alone is enough to use one.

Equations

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