Build and return a :class:`Kernel` backed by this project.

Return the path printed by `lean --print-prefix`.

Allocate a LeanCallableObject of the given variant and bind the closure * (transferring ownership). Wraps the resulting Python object as a Lean * `P

Build the heap type. Returns a NEW reference owned by the global * pointer; subsequent calls return the cached value. */

Add maximization objective (returns handle index).

``"HAdd.hAdd"`` -> nested ``Name.str``.

Return the number of bound variables.

Parse an SMT-LIB2 file. This function is similar to :func:`parse_smt2_string`.

Process Lean source code against the current environment. Returns a multi-line string of new constants per command, separated by ``\\

Serialize expression to string.

Set a parameter value.

Return S-expression representation of assertions.

Get the size of the array.

Shorthand: create solver, add args, check.

Convert to Python string.

Ask `python3` (or `python`) on PATH where its own libpython lives. * This handles pyenv / uv-managed / framework Pythons whose libdir * isn't on the

Check that signed a + b does not underflow.

Check that signed a * b does not underflow.

Reduction AND: 1-bit result, all bits ANDed.

Reduction OR: 1-bit result, all bits ORed.

Check that signed a / b does not overflow (MIN_INT / -1).

Check that signed a - b does not overflow.

Bitwise NAND.

Bitwise NOR.

Bitwise XNOR.

Create multiple (possibly mutually recursive) datatypes.

Regex difference.

Create a disjoint sum datatype. z3py compat: sorts is list[SortRef], ctors named inject0/inject1/..., accessors named project0/project1/...

Tactic that fails if probe is true.

Return size of finite domain sort.

Check if a real value is an integer.

Find last index of substr in s.

Pseudo-boolean equality: sum of (coeff * bool) == k.

Pseudo-boolean >=: sum of (coeff * bool) >= k.

Pseudo-boolean <=: sum of (coeff * bool) <= k.

Add definition to a recursive function.

Remove element from set.

Check if set has exactly n elements.

Create a simple solver (returns standard Solver).

Create a solver for a specific logic (returns standard Solver).

Convert character code to single-char string.

Convert single-char string to character code.

Apply tactic with timeout (timeout ignored — Lean handles timeouts internally).

Update array at index i with value v (alias for Store).

Apply tactic with parameters (parameters ignored — Lean tactics have fixed behavior).

Add convenience helper methods.

Add Python implementations of key static inline functions.

Apply a function/operator to resolved args.

Return the 'declaration name' for an AST node.

Build a Python wrapper around an `@[export]`'d Lean function. Conventions for the C ABI of Lean-exported functions: * Most parameter types

Dynamically create the LeanFFI class with all bindings.

Convert an effectful Term to a Lean proposition string.

Register C smart constructors for Lean kernel types. ``Lean.Name``, ``Lean.Level``, and ``Lean.Expr`` constructors use ``@[extern]`` annotati

Dynamically create ctypes Structure classes from the model.

Convert an effectful VC Term to a ``Lean.Expr`` proposition. Builds ``∀ (x : Int) ..., preconds → body`` with correct de Bruijn indices at ea

Recursively collect uninterpreted sort names from an AST sort.

Generate a minimal Lake project on disk.

Extract a tag like ``v4.29.1`` from the toolchain string.

On macOS, rewrite any `@rpath/libFoo.dylib` references to absolute paths under Lean's `lib/lean`. This lets `dlopen` succeed without a pre-set

Initialise Lean's task manager once per process. `Lean.importModules` (and any kernel operation that allocates a `Task`) asserts on `

Constructors with no payload are encoded as boxed scalars (the tag).