Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

all_builtin_names

Get the full list of all builtin names.

builtin_count

Count the total number of builtin names.

builtin_ctor_count

Return the number of constructors for a builtin inductive type.

builtin_is_prop

Check whether a builtin type is in Prop.

builtin_is_recursive

Check whether a builtin type is recursive.

builtin_universe_level

Return the universe level of a builtin type (0 = Prop, 1 = Type₀).

classify_builtin

Classify a name into its BuiltinKind.

core_builtin_infos

Return info for all core builtin types.

init_builtin_env

Initialize the environment with built-in types and axioms.

is_builtin

Check if a name is a built-in primitive.

is_logical_connective

Check whether a name is a core logical connective.

is_nat_op

Check if a name is a built-in Nat operation.

is_primitive_value

Check whether a name is a primitive value (not a type).

is_string_op

Check if a name is a built-in String operation.

lean4_name

Return the Lean 4 equivalent name for a builtin OxiLean name.

verify_builtins

Check if all builtin names are registered in an environment.