Compile AST to Lean.Expr, create goal, try tactics. Returns True if proved.

Create a string literal.

Prove a claim directly (no double-negation). Returns ``True`` if proved, ``False`` otherwise. Prints "proved" or "failed to prove" to match k

Get element at index.

Declare an uninterpreted function. ``Function('f', IntSort(), IntSort(), BoolSort())`` declares ``f : Int -> Int -> Prop``.

Read from array or apply lambda. Maps to function application in Lean.

Create a string variable.

Regex matching exactly the string s.

Return sort name as string (z3py compat).

Empty set — constant array of False.

Write to array.

If a Python exception is set, fetch a string for it, clear, and return * a Lean IO error result. Caller transfers ownership. */

Convert a ``Lean.Expr`` (as ``LeanInductiveValue``) to a SymPy expression. Handles the elaborated forms that Lean's kernel produces (with type an

Return the sort of the i-th argument.

Build a lambda expression (maps to Lean lambda).

Sign-extend a bit-vector by n bits.

Convert Int to Real.

Rational value a/b as Real division.

Left-fold sum.

Convert a ``Lean.Expr`` (as ``LeanInductiveValue``) to a Z3 expression.

Return the function declaration for this expression.

Number of arguments (children) of this expression.

Parse a string in SMT-LIB2 format. The arguments ``sorts`` and ``decls`` are Python dictionaries used to initialize the symbol table for the

Absolute value via ITE.

String or sequence length.

Concatenate strings.

Apply this tactic to a goal via Pantograph.

Wrap an owned PyObject as IO Py; if NULL, propagate any pending Py error. */

Extract bits [hi:lo] from a bit-vector.

Single-element sequence.

Convert a bit-vector to an integer. If is_signed is False (default, matching z3), uses unsigned (toNat). If is_signed is True, uses signed (t

Constant array (all indices map to ``val``).

Add element to set.

Zero-extend a bit-vector by n bits.

Return the i-th argument of this expression.