Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

check_constant_info

Check a ConstantInfo (inductive, constructor, recursor, or quotient) and add it to the environment.

check_constant_infos

Check multiple ConstantInfo declarations, stopping on the first error.

check_declaration

Check a declaration and add it to the environment.

check_declarations

Check multiple declarations in sequence.

check_declarations_collect_errors

Check multiple declarations, collecting all errors rather than stopping at first.

check_declarations_with_stats

Check multiple declarations and collect statistics.

check_dependencies_exist

Check that all dependencies of a declaration exist in the environment.

declaration_dependencies

Collect the names of all constants referenced in a declaration.

format_batch_result

Format a batch check result for display.

format_decl_summary

Format a declaration summary for display.

has_unique_univ_params

Check that a declaration’s universe parameter list has no duplicates.

is_structurally_valid_expr

Perform a basic structural validity check on an expression.

is_valid_decl_name

Check that a declaration name is valid (non-empty, no invalid characters).

summarize_declaration

Summarize a declaration without checking it.

univ_params_compatible

Check that two universe parameter lists are compatible (same length, same names).

verify_environment_integrity

Check the integrity of an environment by re-type-checking all declarations.