Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

alpha_similar

Check if two expressions differ only in binder names (alpha-equivalent at the surface level, without substitution).

bounded_conversion

Bounded depth search for convertibility.

check_conversion

Perform conversion checking with diagnostics.

contains_subterm

Check if an expression structurally “contains” another as a subterm.

conversion_diff

Collect pairs of subexpressions that differ between two expressions.

convertibility_score

Compute a heuristic convertibility score between 0.0 and 1.0.

count_free_vars

Count the number of distinct free variables in an expression.

def_eq_with_mode

Check if two expressions are definitionally equal with a specified transparency mode.

expr_depth

Depth of an expression tree.

expr_size

Count total number of nodes in an expression tree.

exprs_equal

Check if two expressions are syntactically equal (alias for syntactic_eq).

is_atomic

Check if an expression is in “atomic” form (no reducible subexpressions).

is_beta_normal

Check whether an expression is in normal form: no beta-redexes at top level.

is_eta_equal

Check eta-equality: f and lambda x. f x are eta-equal.

is_leaf

Check if an expression has no subterms at all (is completely atomic).

is_transparency_neutral

Check whether an expression is transparency-neutral.

levels_def_eq

Check if two level expressions are definitionally equivalent.

same_head

Check whether two expressions have the same outermost constructor/head.

structural_distance

Compute the “edit distance” between two expressions as a rough measure of how different they are structurally.

syntactic_eq

Fast syntactic equality check without reduction.