Module callback 

Rust callback handles for Lean-to-Rust interop.

This module is an L1 interop primitive. It owns the Rust side of the callback ABI: handle lifetime, trampoline selection, payload decoding, stale-handle checks, and panic containment. Lean receives two USize values, an opaque handle and the crate-owned trampoline, then calls back into Rust with one of the sealed payload shapes supported by this crate.

The public surface deliberately does not accept a user-supplied function pointer. Callers register a Rust closure and pass the returned LeanCallbackHandle’s ABI values to a Lean export. The handle must stay alive until Lean can no longer call it.

Structs

LeanCallbackHandle

RAII registration for a Rust callback Lean may invoke.

LeanProgressTick

Counter payload for progress-like callback ticks.

LeanStringEvent

String payload delivered by Lean and copied before user code runs.

Enums

LeanCallbackFlow

Flow decision returned by a Rust callback.

LeanCallbackStatus

Status returned by the Rust callback trampoline to Lean.

Traits

LeanCallbackPayload

Payload type accepted by a LeanCallbackHandle.