Add minimization objective (returns handle index).

Nat-specific reasoning.

Return the i-th no-pattern.

Return number of no-patterns (0).

Return number of patterns (0 — patterns not supported).

Open Z3 log file (no-op).

Return parameter descriptions.

Parse a Lean `IO.userError` string produced by `raise_py_error`. The C bridge formats Python errors as `"<TypeName>: <message>"`. If `raw` ma

Return the i-th pattern.

Serialise the goal state to disk via Lean's ``saveModuleData``. Round-trips with :meth:`Kernel.goal_unpickle`. Raises on error.

Return description of a probe.

Process a single SMT-LIB2 command.

Return proof (not supported).

Simple tautologies — the bread and butter of knuckledragger.

Solver backtracking — incremental reasoning.

Return quantifier identifier (empty string).

Uninterpreted sorts + functions — the group theory / syllogism pattern. This is a core knuckledragger idiom: G = smt.DeclareSort("G")

Return reason for unknown result.

Set solver options (no-op — Lean solver has no tunable parameters).

Set global Z3 parameters (no-op — Lean has no tunable Z3 parameters).

Return Skolem identifier (empty string).

Solve using a specific solver instance.

Create a Solver that uses this tactic.

Using the Solver to detect contradictions (unsat). In knuckledragger, you'd use z3.Solver() directly. Here the solver drives grind under the

Return solver statistics.

Return description of a tactic.

Return SMT-LIB2 representation (approximate).

Translate solver to another context (no-op).

Translate expression to another context (no-op — single context).

Equivalent to ``let <binder_name> := <expr_str>``.

Substitute the goal with an expression that may contain sorrys, leaving the sorrys as fresh subgoals.

Equivalent to ``have <binder_name> : <type_str> := ?``.

Equivalent to ``let <binder_name> : <type_str> := ?``.

Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.

Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.

Return unsat core (not supported).

Return the sort of the i-th bound variable.

Verify all ``assert_refined`` calls in *fn* hold given its refinements. 1. Inspect *fn*'s type annotations → create ``defop(int)`` per param +

Return quantifier weight (default 0).

Check that signed negation does not overflow (i.e. a != MIN_INT).

Cube root (represented as application).

Conditional tactic: apply t1 if probe p is true, else t2.

Create a polymorphic datatype builder. Returns a Datatype builder.

Create a datatype sort (alias for DeclareSort).

Get the default value of a constant array. Otherwise build an AppNode.

Mathematical constant e (Euler's number).

Array extensionality: return an index where a and b differ.

Filter finite set s with predicate f.

Map function f over finite set s.

Finite set range (not supported).

Set cardinality (not supported).

Full sequence.

Declare a linear (total) order relation.

Create an infinitesimal value.

Return roots of polynomial (not supported).

Create a new (empty) model.

Declare a partial order relation.

Mathematical constant pi.

Declare a piecewise linear order relation.

Create a propagation function.

Left fold over sequence.

Indexed left fold over sequence.

Map function over sequence.

Map indexed function over sequence.

Create a singleton set containing e.

Extract subsequence (alias for SubString).

Compute the transitive closure of a binary relation.

Declare a tree order relation.

Conditional tactic: apply t when probe p is true.