Walk a ``Lean.Name`` ADT (anonymous / str / num) to a dot-separated string.

Return parameters of this expression (e.g. bit-width for Extract).

Convert an S-expression to an ExprRef.

S-expression representation of this sort.

Check if ``simplify(lhs - rhs) == 0``.

Return the name of the i-th bound variable.

Regex matching any single character.

Character at index i as a single-char string.

At least k of the boolean args are true.

Check that a * b does not overflow.

Check that a - b does not underflow.

Empty sequence / set.

Create a fresh real constant.

String membership in regex.

Check if a is a subset of b.

Bounded repetition.

Quantifier multi-pattern.

Zero or one.

Try first, fall back to subsequent tactics on failure.

Parallel-or — try all tactics in parallel, return first success. Since we run sequentially, this is equivalent to OrElse.

Parallel-then — apply t1, then t2 to each subgoal in parallel. Since we run sequentially, this is equivalent to Then.

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

Declare a recursive function.

Apply tactic repeatedly until fixed point.

Set difference: a \\ b.

Set union via lambda.

Square root (represented as a^(1/2)).

Sequential composition — apply each tactic in order.

Create a de Bruijn indexed variable. Since lean.py uses named variables, this creates a variable named ``__db_<idx>`` with the given sort.

Wrap *expr* in ForAll over declared vars that appear in it.

Decode an `IO.Error` ctor pointer into a typed exception. For `userError` — the most common, used by every `LeanPy.Python.*` bridge f

Wrap a child AST node as an ExprRef with best-effort sort inference.

Compute the ABI memory layout for a constructor's fields. Uses each field wrapper's ``ctor_scalar_size`` to classify fields as pointe

True for ground literal AST nodes (no variables/operations).

Decode a Lean string object pointer into a Python str.

Git rev for the LeanPy Lake dependency when pip-installed. Resolution order: LEANPY_GIT_REV env var, then the commit hash from direct_url.jso

Build an effectful handler that maps Term ops → Lean.Expr builders. *depth* is the number of forallE binders above the expression scope. Vari

Create a ctypes Structure subclass dynamically.

Convert a Python ASTNode to a Lean Z3Expr value.

A wrapper for any Lean type that we can't introspect (Py, kernel `GoalState`, anything not in the `derive_python` registry). Python s

Return a builder for a unary operation (last 1 arg).

Unwrap a ToRealNode wrapper, if present.

Wrap the expression AST in ForAll nodes for its free variables. Sorts free vars: Type vars first, arrows (functions) second, values last.

Return the body of the quantifier.

Return list of all children of this expression.

Extract all `sorry` placeholders in ``source`` as a draftable :class:`GoalState`. Returns ``(state, message)`` — state is ``None`` if

Returns ``"true"`` / ``"false"`` / ``"<undecided>"`` / ``"<elab: ...>"`` etc.

Decode a ``LeanObj`` (raw ``lean_object*``) as a registered inductive. This is the entry point for Path B (tactic): Lean wraps an ``Expr``

Return ctx if not None, else main context.

Get the dynamically created LeanFFI class.

Get de Bruijn index of a bound variable.

Return version string.

Create a new goal state from a ``Lean.Expr`` object. Raises ``LeanError`` on type-check failure.

True if a is a concrete bitvector literal.

True if a is a function declaration.

True for integer division.

Check if result is Ok.