Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

abstract_fvar

Abstract a free variable into a bound variable.

abstract_fvars_ordered

Simultaneously lift all FVars from mapping by replacing them with BVars starting at start_level. The first entry in mapping maps to BVar(start_level), the second to BVar(start_level+1), etc.

alpha_eq

Check if two expressions are alpha-equivalent (identical up to bound variable renaming). This is a simple structural check — it does NOT reduce.

close_with_lambdas

Abstract a list of free variables, turning them into nested lambda binders.

close_with_pis

Abstract a list of free variables, turning them into nested pi binders.

collect_consts

Collect all constant names that appear in an expression (deduplicated).

collect_fvars

Collect all free variables (FVarId) occurring in expr.

count_bvar

Count the number of occurrences of BVar(level) in expr.

count_fvar

Count occurrences of a free variable fv in an expression.

expr_depth

Compute the syntactic depth of an expression (longest path from root to leaf).

expr_size

Compute the number of nodes in the expression tree.

has_bvar

Check if an expression contains a specific bound variable.

has_fvar

Check if an expression contains a specific free variable.

instantiate

Instantiate bound variable with a free variable.

is_closed

Check if an expression is closed (no free BVars at depth 0).

is_ground

Check whether expr is a closed term (no BVars and no FVars).

lift

Lift (shift) all bound variable indices in expr by amount starting from the given cutoff.

lower

Lower (un-shift) all bound variable indices ≥ cutoff by amount.

rename_binder

Rename a bound variable (change binder name without affecting semantics).

subst

Substitute bound variable with an expression.

subst_const

Replace all occurrences of a constant name with another expression.

subst_fvars

Simultaneously substitute multiple free variables with expressions.