Liking cljdoc? Tell your friends :D

ansatz.lean.jvm

Clojure REPL interface to checked Lean project execution. Core Ansatz can be used alongside this optional module; kernel declaration import is separate.

Clojure REPL interface to checked Lean project execution. Core Ansatz can be
used alongside this optional module; kernel declaration import is separate.
raw docstring

ansatz.lean.jvm.argument

Pure host planning for scalar-free managed arguments; no guest allocation or RC operation.

Pure host planning for scalar-free managed arguments; no guest allocation or RC operation.
raw docstring

ansatz.lean.jvm.artifact

Bounded portable native-project artifacts. Reading requires an independent expected manifest digest and performs no native/toolchain discovery.

Bounded portable native-project artifacts. Reading requires an independent
expected manifest digest and performs no native/toolchain discovery.
raw docstring

ansatz.lean.jvm.capabilities

Audited positive task-free profile. Descriptors are metadata, not artifact authority.

Audited positive task-free profile. Descriptors are metadata, not artifact authority.
raw docstring

ansatz.lean.jvm.codec

Type-directed host carriers. Leaf conversion allocates no guest Nodes and can finish before crossing the interpreter's invocation boundary.

Type-directed host carriers. Leaf conversion allocates no guest Nodes and
can finish before crossing the interpreter's invocation boundary.
raw docstring

ansatz.lean.jvm.compiler.bundle

Explicit external Linux producer bundle. SDK pins independently authorize its helpers; bundle self-description alone never authenticates native producers.

Explicit external Linux producer bundle. SDK pins independently authorize its
helpers; bundle self-description alone never authenticates native producers.
raw docstring

ansatz.lean.jvm.compiler.encoding

Bounded exact UTF-8 and JSON parsing shared by the native source producer.

Bounded exact UTF-8 and JSON parsing shared by the native source producer.
raw docstring

ansatz.lean.jvm.compiler.evidence

Actual native build receipt issuer. Definition load does not launch processes. Load once: issued receipt identities survive only in this namespace cohort.

Actual native build receipt issuer. Definition load does not launch processes.
Load once: issued receipt identities survive only in this namespace cohort.
raw docstring

ansatz.lean.jvm.compiler.local

Internal source/compiled-module preparation. No artifact, entry or READY Project is issued here. Uses the fixed compiler's monitored native transport.

Internal source/compiled-module preparation. No artifact, entry or READY
Project is issued here. Uses the fixed compiler's monitored native transport.
raw docstring

ansatz.lean.jvm.compiler.transport

Shared bounded native producer transport. Loaded only by explicit source compilation; precompiled artifact loading does not initialize this service.

Shared bounded native producer transport. Loaded only by explicit source
compilation; precompiled artifact loading does not initialize this service.
raw docstring

ansatz.lean.jvm.construction

Private materialization of a fully validated host plan in one actual engine. The caller must journal returned roots and start under the same Project lease.

Private materialization of a fully validated host plan in one actual engine.
The caller must journal returned roots and start under the same Project lease.
raw docstring

ansatz.lean.jvm.entry

Shared native entry observations. Validating metadata never issues a build, artifact or runtime capability; those issuers retain their own byte custody.

Shared native entry observations. Validating metadata never issues a build,
artifact or runtime capability; those issuers retain their own byte custody.
raw docstring

ansatz.lean.jvm.ir

Internal adapter for the packaged canonical Java interpreter. These wrappers prepare trusted original rows and drive its existing ownership protocol; they do not authenticate source bytes, infer Lean types or establish Init startup. No research interpreter, benchmark, runtime javac or source checkout is used.

Internal adapter for the packaged canonical Java interpreter. These wrappers
prepare trusted original rows and drive its existing ownership protocol; they
do not authenticate source bytes, infer Lean types or establish Init startup.
No research interpreter, benchmark, runtime javac or source checkout is used.
raw docstring

ansatz.lean.jvm.original

Original occurrence-metadata and body-call Header borrowing checks.

Original occurrence-metadata and body-call Header borrowing checks.
raw docstring

ansatz.lean.jvm.preparation

Trusted native source→portable artifact preparation. Never opens a JVM Project or invokes its runtime initializers/main; native compilation can execute metaprograms.

Trusted native source→portable artifact preparation. Never opens a JVM Project
or invokes its runtime initializers/main; native compilation can execute metaprograms.
raw docstring

ansatz.lean.jvm.producer

Pure independently admitted non-entry producer cohorts. Never loads native services.

Pure independently admitted non-entry producer cohorts. Never loads native services.
raw docstring

ansatz.lean.jvm.project

Private issued Project leases behind the Java facade. No raw guest values, native producer receipts or mutable engine aliases cross that facade.

Private issued Project leases behind the Java facade. No raw guest values,
native producer receipts or mutable engine aliases cross that facade.
raw docstring

ansatz.lean.jvm.publisher

Combined program publisher over actual native build receipts. No process launch.

Combined program publisher over actual native build receipts. No process launch.
raw docstring

ansatz.lean.jvm.scalar-buffer

Trusted scalar/buffer codec helpers. Plans contain no guest Nodes. Borrowed decoders acquire/release no credits; the caller retains the actual result root.

Trusted scalar/buffer codec helpers. Plans contain no guest Nodes. Borrowed
decoders acquire/release no credits; the caller retains the actual result root.
raw docstring

ansatz.lean.jvm.signature

Closed application signatures shared by native evidence, artifact validation and host codecs. These are calling descriptors, not inferred erased IR types.

Closed application signatures shared by native evidence, artifact validation
and host codecs. These are calling descriptors, not inferred erased IR types.
raw docstring

ansatz.lean.jvm.startup

Interpreted startup ledger; only the fixed research publisher currently issues Prepared.

Interpreted startup ledger; only the fixed research publisher currently issues Prepared.
raw docstring

ansatz.lean.jvm.value

Borrowed, type-directed result decoding. No guest allocation or RC operation. The caller keeps the actual owned result root until decoding completes.

Borrowed, type-directed result decoding. No guest allocation or RC operation.
The caller keeps the actual owned result root until decoding completes.
raw docstring

cljdoc builds & hosts documentation for Clojure/Script libraries

Keyboard shortcuts
Ctrl+kJump to recent docs
←Move to previous article
→Move to next article
Ctrl+/Jump to the search field
× close