Replace first occurrence of old with new in s.

Convert string to integer.

Convert Real to Int (floor).

Unsigned division.

Unsigned greater-than.

Coerce int/float/BoolRef/ArithRef to ArithRef.

Create appropriately-typed ExprRef subclass for a sort.

Human-readable string for an ASTSort.

Add Lean's `lib/lean` to the OS-level dynamic-loader search path for the current process. Useful before constructing a `LeanLibrary` when the

Conjunction of all constraints.

Structural equality between AST nodes (not SMT equality).

Return a cached managed project, creating it if necessary.

Return the main context.

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

Return number of push scopes.

A compact pseudo-Lean rendering for diagnostics.

Check if a SymPy proposition is identically true.

Convert a function declaration to an array.

At most k of the boolean args are true.

Check that a + b does not overflow.

Complement of regex.

Create a fresh boolean constant.

Intersection of regexes.

Set membership test.

One or more repetitions.

Character range [lo..hi].

Signed remainder.

Set complement via lambda.

Set intersection via lambda.

Set sort — implemented as Array(s, Bool).

Unsigned greater-than-or-equal.

Unsigned remainder.

Union of regexes.

Return child AST nodes of an AST node.

Call *fn* with ``c_void_p`` args, cast result to *ObjPtr*.

Ensure the runtime types are built (lazy init).

Resolve a C type string to a ctypes type, given known struct types.

Walk and replace variables in an AST tree.

Return the signed integer value.

Locate the ``.lean`` source file for ``module_name``.

Return a unique integer identifier for this expression.

Get the dynamically created struct types.

True if a is a function application.

True if a is a concrete integer literal.

True if a is a rational value (division of two integer literals on Real sort).