Documentation
Lean
.
Runtime
Search
return to top
source
Imports
Init.Prelude
Imported by
Lean
.
closureMaxArgsFn
Lean
.
maxSmallNatFn
Lean
.
libUVVersionFn
Lean
.
openSSLVersionFn
Lean
.
closureMaxArgs
Lean
.
maxSmallNat
Lean
.
libUVVersion
Lean
.
openSSLVersion
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_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