z3py-compatible solver interface. ``check()`` builds the conjunction of all assertions, negates it, and tries to prove the negation via grind

Boolean / Prop expression.

Arithmetic expression (Int, Nat, Real).

A named tactic that dispatches to Pantograph.

Base expression node.

Bit-vector expression, maps to Lean's ``BitVec n``.

A pair of py↔lean conversion functions for a particular `TypeRepr`. For types that can appear as inline scalar fields inside a ``lean_ctor_ob

A proof goal — a collection of constraints to be proved.

Probe — measures properties of goals.

SMT array expression, maps to Lean function type.

A Python representation of a Lean inductive constructor. Attributes: ctor: the constructor name (unqualified). tag: integer

Placeholder — Lean is a proof checker, not an SMT solver.

Result of applying a tactic: a list of sub-goals.

Opaque handle to a Lean ``GoalState``. Methods dispatch back into the underlying Lean library.

String expression.

Floating-point expression.

Regex expression.

Refinement: value > n.

The kernel facade. Wraps a :class:`LeanLibrary` whose Lean source has imported ``LeanPy.Kernel`` and exposed the standard ``@[python]`` surfa

Optimization solver. Lean is a proof checker, not an optimization solver, so optimization queries return ``unknown``. Programs that build Opt

Vector of AST nodes.

Uninterpreted function declaration, created via ``Function(...)``.

Map from AST nodes to AST nodes.

Floating-point numeral.

Fixedpoint (Datalog) solver backed by Lean's ``grind`` tactic. Encodes facts as hypotheses and rules as universally-quantified implications,

FP value encoded as IEEE 754 bit pattern (always a non-negative int).

Floating-point rounding mode.

Owned Python-side handle to a Lean object pointer. On construction the object's reference count is *not* incremented — we assume the caller p

Rational numeral — concrete rational value with extraction methods.

Sequence expression.

Character expression.

Z3 context — lean.py uses a single global context.

Integer numeral — concrete integer value with extraction methods.

Build an algebraic datatype backed by a real Lean inductive.

Character sort.

Datatype expression (constructor application result).

A single entry in a function interpretation.

Function interpretation in a model.

Base class for any error raised by lean-py at the FFI boundary. Attributes: kind: short tag identifying the Lean `IO.Error` constructor

Base class for Python-friendly Lean value wrappers.

Wrapper around numeric ExprRef values for z3py compatibility.

Sequence sort.

Base sort.

Solver statistics.

Metaclass for constructor pattern-match classes. Overrides ``isinstance`` so that ``isinstance(value, Name.str)`` returns True when ``value``

SMT array sort, maps to Lean function type ``dom → rng``.

Fixed-width bit-vector sort, maps to Lean's ``BitVec n``.

Sort backed by a Lean inductive type.

Floating-point sort (IEEE 754).

Named FP operation with pre-compiled args (RM already stripped).

Quantified expression (ForAll / Exists).

Real closed field number (not natively supported).