Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

alpha_eq

Check if two expressions are equal after full normalization.

alpha_eq_env

Check if two expressions are equal after full normalization with environment.

count_reduction_steps

Count the number of reduction steps to reach normal form.

evaluate

Evaluate an expression with an environment to a value.

head_normal_form

Reduce an expression to head-normal form without environment (no delta-unfolding).

is_in_whnf

Check if an expression is already in weak head normal form.

is_normal_form

Check if an expression is already in normal form.

normalize

Normalize an expression to full normal form (no environment).

normalize_binders

Normalize only up to n binders deep.

normalize_env

Normalize an expression with an environment.

normalize_fully

Normalize an expression fully, but only up to a given depth limit.

normalize_many

Normalize a slice of expressions in parallel (sequential implementation).

normalize_many_env

Normalize a slice of expressions using an environment.

normalize_selective

Normalize only constants in the expression that appear in the given whitelist.

normalize_types

Normalize only the type-level parts of an expression (sorts and Pi domains).

normalize_whnf

Compute weak head normal form and then fully normalize.

normalize_with_stats

Normalize while collecting statistics.

normalize_with_strategy

Apply a normalization strategy to an expression.

reduce_n_steps

Apply exactly n reduction steps to the expression.