Check if pre is a prefix of s.

Rotate left.

Convert BoolRef to ArithRef via If(b, coeff, 0).

Get a singleton LeanFFI instance.

Parse the multi-line encoding produced by Lean's ``encodeTacticResult``.

Check if s contains t.

The i-th ctor field as a raw lean_object pointer.

Load a Lean library from a Lake project directory. Looks for `<lake_dir>/.lake/build/lib/lib<library_name>.<ext>` (or, when `library_

Concatenate two or more bit-vectors (left-fold).

Logical (unsigned) shift right.

Check if suf is a suffix of s.

Unsigned less-than-or-equal.

Create a new goal state from a type expression string. Raises ``LeanError`` on parse / elaboration failure.

Create a fresh constant with a unique name.

Full set — constant array of True.

Left-fold product.

Rotate right.

Convert a Python ASTSort to a Lean Z3Sort value.

Return the number of arguments.

Return sort kind as integer (z3py compat). Values match z3 Z3_sort_kind: UNINTERPRETED=0, BOOL=1, INT=2, REAL=3, BV=4, ARRAY=5, DATAT

Return the range (return) sort.

Convert an S-expression to a SortRef.

Run a command and return the trimmed stdout.

Simplify an expression (placeholder — returns input unchanged).

Substitute expressions: substitute(t, (old1, new1), (old2, new2), ...). Each pair (old, new) replaces occurrences of old with new in t. old m

Create a fresh integer constant.

Unsigned less-than.

Tag of a Lean object — works for both scalar (enum) and pointer (ctor) forms.

Convert any ctypes pointer-like value to a raw integer. macOS ctypes has a long-standing quirk: passing a `POINTER(struct)` instance directly

Find index of substr in s starting at offset.

Signed division.

General sequence sort. For Char, returns StringSort.

Kleene star.

Extract substring.

Create a tuple sort. Returns (sort, constructor, list_of_accessor_FuncDeclRefs). z3py compat: ctor name = sort name, accessors named project0

Human-readable string for an ASTNode (for debugging).

Return a builder for a binary operation (last 2 args).

Declare that *value* satisfies *refinement*. During symbolic execution, the handler intercepts this and collects the verification condition a

True if a is an arithmetic expression (Int, Nat, or Real).

True if a is a sort reference.

Where Lean's own shared libraries live.

Set the global kernel used by solvers and ``prove()``.

Arithmetic shift right (sign-extending).

Create a vector of ``sz`` boolean variables.

Create an enumeration sort. Returns (sort, list_of_enum_constants).

Convert an integer to a bit-vector of width n.

Convert integer to string.

Create a vector of ``sz`` integer variables named prefix__0, ..., prefix__sz-1.

Apply f element-wise over arrays, producing a new array.

Repeat a bit-vector n times by concatenation.