Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app_depth

Count the nesting depth of applications.

apply_bvars

Apply n BVar arguments to an expression: expr BVar(0) BVar(1) ... BVar(n-1).

arity

Attempt to compute the arity of an expression by counting Pi binders.

beta_reduce_full

Apply beta reduction repeatedly until no redex exists at the top level.

beta_reduce_one

Substitute replacement for the outermost bound variable (BVar(0)).

binder_depth

Count the number of leading lambda binders.

collect_app_spine

Collect the spine of an application: (head, [arg1, arg2, …]).

contains_bvar

Check if an expression contains a specific bound variable at the given De Bruijn index.

count_bvar

Count occurrences of a bound variable in an expression.

eta_contract

Perform one step of eta contraction.

eta_contract_full

Fully eta-contract an expression.

eta_def_eq

Determine if two expressions are definitionally equal under eta.

eta_equiv

Check eta equivalence (normalize then compare).

eta_equiv_depth

Check whether two expressions are eta-equivalent up to the given depth.

eta_expand

Perform eta expansion: given f, produce λx. f x.

eta_expand_implicit

Perform eta expansion with an implicit binder.

eta_expand_pi

Eta-expand a term with an explicit Pi binder.

eta_expand_to

Eta-expand an expression to match a target number of lambda binders.

eta_expand_with_ty

Expand an expression to exactly n lambda binders using eta expansion.

eta_head

Return the “eta-head” of an expression.

eta_normalize

Eta-normalize an expression (recursively eta-contracting).

eta_normalize_tracked

Eta-normalize and track how many contractions were performed.

expr_is_closed

Check if an expression has no free variables using a recursive walk.

expr_structure_desc

Produce a one-line human-readable description of an expression’s structure.

is_beta_redex

Check whether an expression is a beta-redex (lambda applied to an argument).

is_closed

Check whether an expression is completely closed (no BVars and no FVars).

is_closed_at

Check whether an expression is closed (no free BVars at depth >= cutoff).

is_eta_expandable

Check whether an expression can be eta-expanded (not already a lambda).

is_eta_long

Check whether an expression is in eta-long normal form.

is_eta_redex

Check whether an expression is an eta-redex (λx. f x with x not free in f).

is_identity_lambda

Check if a lambda body is the identity (lambda x. x).

is_lambda_free

Check whether an expression has no lambdas anywhere in it.

is_simple_app

Check whether an expression is a “simple” application (head is a constant).

lam_to_pi

Replace all lambda binders in expr with pi binders (unsafe structural change).

mk_app_spine

Apply a sequence of arguments to a head expression.

node_count

Count the total number of nodes in an expression tree.

normal_eq

Check structural equality after full normalization.

normalize_full

Normalize by both eta-contracting and beta-reducing.

outer_lambda_depth

Count the maximum lambda depth (outermost consecutive lambdas).

peel_lambdas

Peel off all leading lambdas, returning binders and body.

peel_pis

Collect the Pi binders of a type, returning (binders, return_type).

pi_depth

Count the number of leading Pi binders.

rebuild_lam

Rebuild a lambda from peeled binders and a body.

rebuild_pi

Rebuild a Pi from peeled binders and a body.

reduce_let

Reduce let x := v in body to body[x := v].

reduce_lets

Fully reduce all let bindings in an expression.

rewrite_with_rules

Apply a list of rewrite rules to an expression, innermost-first.

shift_down

Shift down bound variables (for removing a binder).

shift_up

Shift up bound variables (for adding a binder).

structural_hash

Compute a simple structural hash of an expression.

subst_bvar

Substitute replacement for BVar(depth) in expr.

subst_bvar_shifted

Lift a substitution under n binders (shift the replacement up by n).

wrap_in_lambdas

Wrap an expression in n identity lambdas: λ_0. λ_1. ... expr.