Runtime coverage

leanprover/lean4:v4.35.0 · generated 2026-10-28

Most of the libraries that ship with Lean—Init, Std, and Lean—compile to JavaScript like any other Lean code. The exceptions are externs: functions that native Lean implements in C, which the LeanScript runtime has to implement in JavaScript instead. Of the 907 externs that a program can call, this page shows which ones the runtime implements on each target.

Externs that a Lean declaration implements through @[export] aren't counted, since the compiler calls that declaration instead.

Library	Node	Browser
Init	92.3%599 / 649	88.3%573 / 649
Std	0.0%0 / 100	0.0%0 / 100
Lean	0.0%0 / 158	0.0%0 / 158
Total	66.0%599 / 907	63.2%573 / 907

Every targetSome targetsNot implemented

InitNode 599/649 · Browser 573/649

FloatNode 57/57Browser 57/57

Float32Node 57/57Browser 57/57

StringNode 30/30Browser 30/30

USizeNode 29/29Browser 29/29

UInt16Node 27/27Browser 27/27

UInt32Node 27/27Browser 27/27

UInt64Node 27/27Browser 27/27

UInt8Node 27/27Browser 27/27

ISizeNode 25/25Browser 25/25

Int16Node 25/25Browser 25/25

Int32Node 25/25Browser 25/25

Int64Node 25/25Browser 25/25

Int8Node 25/25Browser 25/25

ArrayNode 22/22Browser 22/22

IONode 17/21Browser 14/21

7 not on every target

IO.appPath no target
IO.currentDir Node only
IO.getNumHeartbeats no target
IO.getStdin Node only
IO.getTID no target
IO.setNumHeartbeats no target
IO.setStdin Node only

NatNode 21/21Browser 21/21

ByteArrayNode 19/19Browser 19/19

IntNode 16/16Browser 16/16

(top level)Node 14/14Browser 14/14

FloatArrayNode 0/14Browser 0/14

14 not on every target

FloatArray.data no target
FloatArray.emptyWithCapacity no target
FloatArray.get no target
FloatArray.get! no target
FloatArray.markLinear no target
FloatArray.mk no target
FloatArray.propagateMark no target
FloatArray.push no target
FloatArray.set no target
FloatArray.set! no target
FloatArray.size no target
FloatArray.uget no target
FloatArray.uset no target
FloatArray.usize no target

IO.FS.HandleNode 9/12Browser 0/12

12 not on every target

String.Pos.RawNode 11/11Browser 11/11

BoolNode 10/10Browser 10/10

IO.FSNode 6/8Browser 0/8

8 not on every target

String.InternalNode 8/8Browser 8/8

IO.ProcessNode 5/6Browser 0/6

6 not on every target

System.PlatformNode 4/6Browser 4/6

2 not on every target

System.Platform.getIsLinux no target
System.Platform.getTarget no target

IO.Process.ChildNode 0/5Browser 0/5

5 not on every target

Lean.versionNode 0/5Browser 0/5

5 not on every target

ST.Prim.RefNode 5/5Browser 5/5

TaskNode 5/5Browser 5/5

RuntimeNode 0/4Browser 0/4

4 not on every target

BaseIONode 3/3Browser 3/3

IO.PromiseNode 3/3Browser 3/3

System.FilePathNode 3/3Browser 0/3

3 not on every target

System.FilePath.metadata Node only
System.FilePath.readDir Node only
System.FilePath.symlinkMetadata Node only

ThunkNode 3/3Browser 3/3

Lean.InternalNode 0/2Browser 0/2

2 not on every target

Lean.Internal.hasLLVMBackend no target
Lean.Internal.isStage0 no target

ShareCommon.ObjectNode 0/2Browser 0/2

2 not on every target

ShareCommon.Object.eq no target
ShareCommon.Object.hash no target

String.PosNode 2/2Browser 2/2

String.SliceNode 2/2Browser 2/2

CharNode 1/1Browser 1/1

IO.OptionNode 1/1Browser 1/1

IO.PrimNode 0/1Browser 0/1

1 not on every target

IO.Prim.setAccessRights no target

LeanNode 0/1Browser 0/1

1 not on every target

Lean.getGithash no target

Lean.NameNode 0/1Browser 0/1

1 not on every target

Lean.Name.beq no target

ST.PrimNode 1/1Browser 1/1

ShareCommonNode 0/1Browser 0/1

1 not on every target

ShareCommon.shareCommon' no target

ShareCommon.StateNode 0/1Browser 0/1

1 not on every target

ShareCommon.State.shareCommon no target

String.Slice.Pattern.InternalNode 1/1Browser 1/1

System.Platform.InternalNode 0/1Browser 0/1

1 not on every target

System.Platform.Internal.getHardwareConcurrency no target

VoidNode 1/1Browser 1/1

StdNode 0/100 · Browser 0/100

Std.Internal.UV.SystemNode 0/28Browser 0/28

28 not on every target

Std.Internal.UV.System.availableMemory no target
Std.Internal.UV.System.chdir no target
Std.Internal.UV.System.constrainedMemory no target
Std.Internal.UV.System.cpuInfo no target
Std.Internal.UV.System.cwd no target
Std.Internal.UV.System.exePath no target
Std.Internal.UV.System.freeMemory no target
Std.Internal.UV.System.getProcessTitle no target
Std.Internal.UV.System.getrusage no target
Std.Internal.UV.System.hrtime no target
Std.Internal.UV.System.osEnviron no target
Std.Internal.UV.System.osGetGroup no target
Std.Internal.UV.System.osGetHostname no target
Std.Internal.UV.System.osGetPasswd no target
Std.Internal.UV.System.osGetPid no target
Std.Internal.UV.System.osGetPpid no target
Std.Internal.UV.System.osGetPriority no target
Std.Internal.UV.System.osGetenv no target
Std.Internal.UV.System.osHomedir no target
Std.Internal.UV.System.osSetPriority no target
Std.Internal.UV.System.osSetenv no target
Std.Internal.UV.System.osTmpdir no target
Std.Internal.UV.System.osUname no target
Std.Internal.UV.System.osUnsetenv no target
Std.Internal.UV.System.random no target
Std.Internal.UV.System.setProcessTitle no target
Std.Internal.UV.System.totalMemory no target
Std.Internal.UV.System.uptime no target

Std.Internal.UV.TCP.SocketNode 0/16Browser 0/16

16 not on every target

Std.Internal.UV.TCP.Socket.accept no target
Std.Internal.UV.TCP.Socket.bind no target
Std.Internal.UV.TCP.Socket.cancelAccept no target
Std.Internal.UV.TCP.Socket.cancelRecv no target
Std.Internal.UV.TCP.Socket.connect no target
Std.Internal.UV.TCP.Socket.getPeerName no target
Std.Internal.UV.TCP.Socket.getSockName no target
Std.Internal.UV.TCP.Socket.keepAlive no target
Std.Internal.UV.TCP.Socket.listen no target
Std.Internal.UV.TCP.Socket.new no target
Std.Internal.UV.TCP.Socket.noDelay no target
Std.Internal.UV.TCP.Socket.recv? no target
Std.Internal.UV.TCP.Socket.send no target
Std.Internal.UV.TCP.Socket.shutdown no target
Std.Internal.UV.TCP.Socket.tryAccept no target
Std.Internal.UV.TCP.Socket.waitReadable no target

Std.Internal.UV.UDP.SocketNode 0/15Browser 0/15

15 not on every target

Std.Internal.UV.UDP.Socket.bind no target
Std.Internal.UV.UDP.Socket.cancelRecv no target
Std.Internal.UV.UDP.Socket.connect no target
Std.Internal.UV.UDP.Socket.getPeerName no target
Std.Internal.UV.UDP.Socket.getSockName no target
Std.Internal.UV.UDP.Socket.new no target
Std.Internal.UV.UDP.Socket.recv no target
Std.Internal.UV.UDP.Socket.send no target
Std.Internal.UV.UDP.Socket.setBroadcast no target
Std.Internal.UV.UDP.Socket.setMembership no target
Std.Internal.UV.UDP.Socket.setMulticastInterface no target
Std.Internal.UV.UDP.Socket.setMulticastLoop no target
Std.Internal.UV.UDP.Socket.setMulticastTTL no target
Std.Internal.UV.UDP.Socket.setTTL no target
Std.Internal.UV.UDP.Socket.waitReadable no target

Std.BaseSharedMutexNode 0/7Browser 0/7

7 not on every target

Std.BaseSharedMutex.new no target
Std.BaseSharedMutex.read no target
Std.BaseSharedMutex.tryRead no target
Std.BaseSharedMutex.tryWrite no target
Std.BaseSharedMutex.unlockRead no target
Std.BaseSharedMutex.unlockWrite no target
Std.BaseSharedMutex.write no target

Std.Internal.UV.TimerNode 0/5Browser 0/5

5 not on every target

Std.Internal.UV.Timer.cancel no target
Std.Internal.UV.Timer.mk no target
Std.Internal.UV.Timer.next no target
Std.Internal.UV.Timer.reset no target
Std.Internal.UV.Timer.stop no target

Std.BaseMutexNode 0/4Browser 0/4

4 not on every target

Std.BaseRecursiveMutexNode 0/4Browser 0/4

4 not on every target

Std.BaseRecursiveMutex.lock no target
Std.BaseRecursiveMutex.new no target
Std.BaseRecursiveMutex.tryLock no target
Std.BaseRecursiveMutex.unlock no target

Std.CondvarNode 0/4Browser 0/4

4 not on every target

Std.Internal.UV.SignalNode 0/4Browser 0/4

4 not on every target

Std.Internal.UV.Signal.cancel no target
Std.Internal.UV.Signal.mk no target
Std.Internal.UV.Signal.next no target
Std.Internal.UV.Signal.stop no target

Std.Internal.UV.DNSNode 0/2Browser 0/2

2 not on every target

Std.Internal.UV.DNS.getAddrInfo no target
Std.Internal.UV.DNS.getNameInfo no target

Std.Internal.UV.LoopNode 0/2Browser 0/2

2 not on every target

Std.Internal.UV.Loop.alive no target
Std.Internal.UV.Loop.configure no target

Std.Net.IPv4AddrNode 0/2Browser 0/2

2 not on every target

Std.Net.IPv4Addr.ofString no target
Std.Net.IPv4Addr.toString no target

Std.Net.IPv6AddrNode 0/2Browser 0/2

2 not on every target

Std.Net.IPv6Addr.ofString no target
Std.Net.IPv6Addr.toString no target

Std.Time.Database.WindowsNode 0/2Browser 0/2

2 not on every target

Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt no target
Std.Time.Database.Windows.getNextTransition no target

ByteSliceNode 0/1Browser 0/1

1 not on every target

ByteSlice.beq no target

Std.NetNode 0/1Browser 0/1

1 not on every target

Std.Net.interfaceAddresses no target

Std.Time.TimestampNode 0/1Browser 0/1

1 not on every target

Std.Time.Timestamp.now no target

LeanNode 0/158 · Browser 0/158

Lean.LLVMNode 0/81Browser 0/81

81 not on every target

Lean.LLVM.addAttributeAtIndex no target
Lean.LLVM.addCase no target
Lean.LLVM.addFunction no target
Lean.LLVM.addGlobal no target
Lean.LLVM.appendBasicBlockInContext no target
Lean.LLVM.arrayType no target
Lean.LLVM.buildAdd no target
Lean.LLVM.buildAlloca no target
Lean.LLVM.buildBr no target
Lean.LLVM.buildCall2 no target
Lean.LLVM.buildCondBr no target
Lean.LLVM.buildGEP2 no target
Lean.LLVM.buildGlobalString no target
Lean.LLVM.buildICmp no target
Lean.LLVM.buildInBoundsGEP2 no target
Lean.LLVM.buildLoad2 no target
Lean.LLVM.buildMul no target
Lean.LLVM.buildNot no target
Lean.LLVM.buildPtrToInt no target
Lean.LLVM.buildRet no target
Lean.LLVM.buildSext no target
Lean.LLVM.buildSextOrTrunc no target
Lean.LLVM.buildStore no target
Lean.LLVM.buildSub no target
Lean.LLVM.buildSwitch no target
Lean.LLVM.buildUnreachable no target
Lean.LLVM.buildZext no target
Lean.LLVM.clearInsertionPosition no target
Lean.LLVM.constArray no target
Lean.LLVM.constInt no target
Lean.LLVM.constPointerNull no target
Lean.LLVM.constString no target
Lean.LLVM.countBasicBlocks no target
Lean.LLVM.countParams no target
Lean.LLVM.createBuilderInContext no target
Lean.LLVM.createContext no target
Lean.LLVM.createMemoryBufferWithContentsOfFile no target
Lean.LLVM.createModule no target
Lean.LLVM.createStringAttribute no target
Lean.LLVM.createTargetMachine no target
Lean.LLVM.disposeModule no target
Lean.LLVM.disposeTargetMachine no target
Lean.LLVM.doubleTypeInContext no target
Lean.LLVM.floatTypeInContext no target
Lean.LLVM.functionType no target
Lean.LLVM.getBasicBlockParent no target
Lean.LLVM.getDefaultTargetTriple no target
Lean.LLVM.getEntryBasicBlock no target
Lean.LLVM.getFirstFunction no target
Lean.LLVM.getFirstGlobal no target
Lean.LLVM.getFirstInstruction no target
Lean.LLVM.getInsertBlock no target
Lean.LLVM.getNamedFunction no target
Lean.LLVM.getNamedGlobal no target
Lean.LLVM.getNextFunction no target
Lean.LLVM.getNextGlobal no target
Lean.LLVM.getParam no target
Lean.LLVM.getTargetFromTriple no target
Lean.LLVM.getUndef no target
Lean.LLVM.intTypeInContext no target
Lean.LLVM.isDeclaration no target
Lean.LLVM.linkModules no target
Lean.LLVM.llvmInitializeTargetInfo no target
Lean.LLVM.moduleToString no target
Lean.LLVM.opaquePointerTypeInContext no target
Lean.LLVM.parseBitcode no target
Lean.LLVM.pointerType no target
Lean.LLVM.positionBuilderAtEnd no target
Lean.LLVM.positionBuilderBefore no target
Lean.LLVM.printModuletoFile no target
Lean.LLVM.printModuletoString no target
Lean.LLVM.setDLLStorageClass no target
Lean.LLVM.setInitializer no target
Lean.LLVM.setLinkage no target
Lean.LLVM.setTailCall no target
Lean.LLVM.setVisibility no target
Lean.LLVM.targetMachineEmitToFile no target
Lean.LLVM.typeOf no target
Lean.LLVM.verifyModule no target
Lean.LLVM.voidType no target
Lean.LLVM.writeBitcodeToFile no target

Lean.ExprNode 0/21Browser 0/21

21 not on every target

Lean.Expr.abstract no target
Lean.Expr.abstractRange no target
Lean.Expr.data no target
Lean.Expr.dbgToString no target
Lean.Expr.equal no target
Lean.Expr.eqv no target
Lean.Expr.findExtImpl? no target
Lean.Expr.findImpl? no target
Lean.Expr.hasLooseBVar no target
Lean.Expr.instantiate no target
Lean.Expr.instantiate1 no target
Lean.Expr.instantiateRange no target
Lean.Expr.instantiateRev no target
Lean.Expr.instantiateRevRange no target
Lean.Expr.liftLooseBVars no target
Lean.Expr.lowerLooseBVars no target
Lean.Expr.lt no target
Lean.Expr.mkAppData no target
Lean.Expr.mkData no target
Lean.Expr.quickLt no target
Lean.Expr.replaceImpl no target

LeanNode 0/20Browser 0/20

20 not on every target

Lean.closureMaxArgsFn no target
Lean.displayCumulativeProfilingTimes no target
Lean.getMaxCtorFields no target
Lean.getMaxCtorScalarsSize no target
Lean.getMaxCtorTag no target
Lean.getUSizeSize no target
Lean.instantiateExprMVarsImp no target
Lean.instantiateLevelMVarsImp no target
Lean.libUVVersionFn no target
Lean.maxSmallNatFn no target
Lean.mkCasesOnImp no target
Lean.openSSLVersionFn no target
Lean.profileit no target
Lean.runInit no target
Lean.runModInitCore no target
Lean.getManualRoot no target
Lean.decodeLossyUTF8 no target
Lean.emitLLVM no target
Lean.initLLVM no target
Lean.runMain no target

Lean.InternalNode 0/14Browser 0/14

14 not on every target

Lean.Internal.enableDebug no target
Lean.Internal.getBelieverTrustLevel no target
Lean.Internal.getBuildType no target
Lean.Internal.getDefaultMaxHeartbeat no target
Lean.Internal.getDefaultMaxMemory no target
Lean.Internal.getDefaultVerbose no target
Lean.Internal.getOptionOverrides no target
Lean.Internal.hasAddressSanitizer no target
Lean.Internal.isDebug no target
Lean.Internal.isMultiThread no target
Lean.Internal.setExitOnPanic no target
Lean.Internal.setMaxHeartbeat no target
Lean.Internal.setMaxMemory no target
Lean.Internal.setThreadStackSize no target

Lean.Compiler.FFINode 0/4Browser 0/4

4 not on every target

Lean.Compiler.FFI.getBuiltinInternalLinkerFlags no target
Lean.Compiler.FFI.getBuiltinLinkerFlags no target
Lean.Compiler.FFI.getLeancExtraFlags no target
Lean.Compiler.FFI.getLeancInternalFlags no target

Lean.CompactedRegionNode 0/3Browser 0/3

3 not on every target

Lean.EnvironmentNode 0/3Browser 0/3

3 not on every target

Lean.Environment.addDeclCheck no target
Lean.Environment.addDeclWithoutChecking no target
Lean.Environment.evalConstCore no target

Lean.KernelNode 0/3Browser 0/3

3 not on every target

Lean.DynlibNode 0/2Browser 0/2

2 not on every target

Lean.Dynlib.get? no target
Lean.Dynlib.load no target

Lean.Kernel.EnvironmentNode 0/2Browser 0/2

2 not on every target

Lean.Kernel.Environment.addDeclCore no target
Lean.Kernel.Environment.addDeclWithoutChecking no target

Lean.LevelNode 0/2Browser 0/2

2 not on every target

Lean.Level.beq no target
Lean.Level.mkData no target

Lean.BinderInfoNode 0/1Browser 0/1

1 not on every target

Lean.BinderInfo.toUInt64 no target

Lean.Dynlib.SymbolNode 0/1Browser 0/1

1 not on every target

Lean.Dynlib.Symbol.runAsInit no target

Lean.LLVM.ValueNode 0/1Browser 0/1

1 not on every target

Lean.LLVM.Value.getName no target