Return the installed lean_py package version.

Return all globally-exported `initialize_*` symbols in `dylib`. Used as a fallback when the canonical `initialize_<lib>` symbol isn't where w

Convert a BinOp string to a Lean Z3BinOp value.

Convert a UnOp string to a Lean Z3UnOp value.

Handle ``OfNat.ofNat`` — args[1] is the nat literal.

Handle ``OfNat.ofNat`` — args[1] is the nat literal.

Parse all top-level S-expressions from a string.

Parse one S-expression from tokens starting at pos.

Run cc -E and clean output for pycparser.

Wrapper for the `pyobject` TypeRepr (Lean's `LeanPy.Python.Py`). When Lean returns a `Py`, the Lean side hands us a `lean_object*` wr

Build a Lean Array from a Python iterable. Returns owned ptr.

Build a Lean string object from a Python str. Returns owned ptr.

Register a Lean inductive type in the kernel environment.

Handle ((_ op params...) args...).

Resolve the module-initializer symbol, allowing for the Lake-naming variations Lean has gone through. The canonical name is `initiali

Create a SortRef from an ASTSort.

Decode field `idx` of `ptr` as a Lean string (best effort).

Tokenize an SMT-LIB2 string into a flat list of tokens.

Create a goal from a ``Lean.Expr`` and close it. Uses ``simp [Int.ofNat]`` to normalise the fully-elaborated Int literals before ``omega`` de

Wrap an AST node into the correct ExprRef subclass based on sort.

All shared libs in `lib/lean` that are likely needed at load time. Includes `libleanshared`, `libleanshared_*`, `libLake_shared`, and any oth

Disjunction of sub-goal conjunctions (any sub-goal suffices).

Return the integer value as a Python int.

Return the unsigned integer value.

Add assertion tracked by p (tracking ignored — no unsat core support).

Check satisfiability (always returns unknown for optimization).

Check a proposition via Knuckledragger (backed by Z3).

Compute consequences (not supported).

Generate cubes (not supported).

Disable Z3 tracing (no-op).

Enable Z3 tracing (no-op — Lean has its own tracing).

Extract integer #define constants from raw header.

Locate `libleanshared.<ext>` in the active toolchain's `lib/lean`. Set ``LEANPY_LIBLEAN`` to override — useful for pointing at an ASAN-instru

Locate lean.h via the active Lean toolchain. Strategy: 1. Ask `lean --print-prefix` for the toolchain sysroot, look for `<prefix>/

Convert an `IO.Error` payload into a printable C string. The bridge's * own errors are `userError String`; for others we fall back to the * underlyi

Load solver from file (not supported).

Load solver from string (not supported).

Get the extracted constants.

Parse lean.h and return the HeaderModel, using a disk cache for speed.

Return version tuple.

Load a goal state previously serialised with :meth:`GoalState.pickle`.

Return solver help string.

Linear arithmetic — where omega shines.

Return the lean-toolchain string (e.g. ``leanprover/lean4:v4.29.1``). Reads from the repo-root ``lean-toolchain`` file if available, otherwis

Build and return a :class:`LeanLibrary` for this project.