Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

all_alpha_equiv

Check if a list of expressions are pairwise alpha-equivalent.

alpha_class_rep

Compute an alpha-equivalence class representative.

alpha_equiv

Check if two expressions are alpha equivalent.

alpha_equiv_mod_levels

Check if two expressions are alpha equivalent modulo universe levels.

alpha_equiv_under_subst

Check alpha equivalence under a partial FVar substitution.

alpha_hash

Compute a structural hash of an expression for alpha-equivalence purposes.

alpha_subst

Perform capture-avoiding substitution: replace BVar(0) with replacement throughout body, adjusting de Bruijn indices appropriately.

apply_fvar_subst

Apply a map of FVar substitutions to an expression.

bvar0_free

Check whether BVar(0) occurs at all in body.

canonicalize

Rename bound variables in an expression to canonical names. This produces a canonical form for alpha-equivalent expressions.

count_bvar0_occurrences

Count the number of occurrences of BVar(0) in expr (at the current depth).

find_non_equiv_pair

Find the first pair of alpha-non-equivalent expressions in a list.

free_fvars

Collect all free variable IDs occurring in expr.

fvar_occurs

Check if FVar(id) occurs free in expr.

lift

Shift all free de Bruijn indices up by 1 (lift by one binder).

lower

Shift all free de Bruijn indices down by 1 (used after substituting under a binder).

rename_bvar

Rename a specific bound variable index in an expression.

shift

Shift all free de Bruijn indices in expr by amount.

structurally_equal

Structural equality: same as alpha_equiv but uses a simpler name-blind comparison.

swap_bvars

Swap two bound variable indices in an expression.