Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

abstract_fvars

Abstract multiple free variables simultaneously.

abstract_fvars_ordered

Abstract over free variables in dependency order.

abstract_single

Abstract a single free variable, converting it to BVar(0).

apply_beta

Apply multiple arguments to a lambda, performing beta reduction.

bvars_in_range

Check whether all bound variable indices are within valid range for a well-formed expression.

cheap_beta_reduce

Cheap beta reduction: reduce (λ x. body) arg to body[arg/x].

collect_app

Collect function and all arguments from a nested application.

collect_fvars

Collect all free variable IDs occurring in an expression.

count_fvar_occurrences

Count how many times a free variable appears in an expression.

distinct_const_count

Compute the number of distinct names (constants) in an expression.

is_closed_under

Check if an expression is closed under a given set of free variables.

is_ground

Check if an expression is “ground” — no free or bound variables.

lam_arity

Count the number of leading lambda binders.

let_abstract

Abstract a single free variable and simultaneously replace it with a let-binding.

let_abstract_many

Let-abstract multiple bindings in sequence.

max_bvar

Compute the maximum bound variable index in an expression.

mk_app

Build a nested application from a function and a list of arguments.

mk_forall

Build a Pi type from free variables.

mk_lambda

Build a lambda abstraction from free variables.

pi_arity

Count the number of leading pi binders.

rename_const

Rename all occurrences of old_name constant to new_name.

replace_nat_lit

Replace all literal naturals with a given value.

shift_bvars

Shift all bound variable indices >= cutoff by amount.

split_lam

Split a lambda: extract the type and body.

split_pi

Split a pi type: extract the domain and codomain.

subst_fvar

Replace a free variable with a given expression.

topo_sort_fvars

Topological sort of free variables by dependency.