Lean.Runtime

source

@[extern lean_closure_max_args]

opaque Lean.closureMaxArgsFn :

Unit → Nat

source

@[extern lean_max_small_nat]

opaque Lean.maxSmallNatFn :

Unit → Nat

source

@[extern lean_get_max_ctor_fields]

opaque Lean.getMaxCtorFields :

Unit → Nat

source

def Lean.maxCtorFields :

Nat

Equations

Lean.maxCtorFields = Lean.getMaxCtorFields ()

Instances For

source

@[extern lean_get_max_ctor_scalars_size]

opaque Lean.getMaxCtorScalarsSize :

Unit → Nat

source

def Lean.maxCtorScalarsSize :

Nat

Equations

Lean.maxCtorScalarsSize = Lean.getMaxCtorScalarsSize ()

Instances For

source

@[extern lean_get_max_ctor_tag]

opaque Lean.getMaxCtorTag :

Unit → Nat

source

def Lean.maxCtorTag :

Nat

Equations

Lean.maxCtorTag = Lean.getMaxCtorTag ()

Instances For

source

@[extern lean_get_usize_size]

opaque Lean.getUSizeSize :

Unit → Nat

source

def Lean.usizeSize :

Nat

Equations

Lean.usizeSize = Lean.getUSizeSize ()

Instances For

source

@[extern lean_libuv_version]

opaque Lean.libUVVersionFn :

Unit → Nat

source

@[extern lean_openssl_version]

opaque Lean.openSSLVersionFn :

Unit → Nat

source

def Lean.closureMaxArgs :

Nat

Equations

Lean.closureMaxArgs = Lean.closureMaxArgsFn ()

Instances For

source

def Lean.maxSmallNat :

Nat

Equations

Lean.maxSmallNat = Lean.maxSmallNatFn ()

Instances For

source

def Lean.libUVVersion :

Nat

Equations

Lean.libUVVersion = Lean.libUVVersionFn ()

Instances For

source

def Lean.openSSLVersion :

Nat

Equations

Lean.openSSLVersion = Lean.openSSLVersionFn ()

Instances For