Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

abstract_expr

Replace FVar with BVar(0), shifting up all existing BVars.

apply_args

Apply a list of arguments to a function expression via beta reduction.

beta_reduce_head

Repeatedly apply top-level beta reduction until no more is possible.

build_subst_map

Build a SubstMap from parallel slices of ids and replacements.

collect_loose_bvar_indices

Collect the indices of all loose bound variables.

count_free_occurrences

Count how many times fvar occurs free in expr.

count_lambdas

Count the number of leading lambda binders.

count_pis

Count the number of leading pi binders.

expr_contains_fvar

Check if an expression contains any free variable in the given set.

free_vars

Collect the set of free FVarIds occurring in expr.

instantiate

Instantiate BVar(0) with arg in body, shifting down all other BVars.

instantiate_many

Simultaneously substitute BVar(0)..BVar(k-1) with args[0]..args[k-1].

instantiate_tracked

Like instantiate but also fills in SubstStats.

is_lambda

Check if an expression is a lambda abstraction.

is_whnf_beta

Check whether expr is in weak head normal form with respect to beta.

occurs_free

Return true if fvar occurs free in expr.

open_binder

Replace the outermost BVar(0) of a body with FVar(id) (open a binder).

parallel_subst

Apply a parallel substitution: replace each FVar(id) with the corresponding expression in map.

parallel_subst_tracked

Apply a parallel substitution and collect profiling statistics.

peel_lambdas

Peel off n leading lambda binders, collecting binder info.

shift_bvars

Shift all BVar(i) with i >= cutoff up by amount.

subst_fvar

Substitute a single free variable with an expression.

substitute_fvars

Apply a substitution list (as parallel arrays) to an expression.

try_beta_reduce

Apply beta-reduction once at the top level if possible.

Type Aliases

SubstMap

A finite mapping from free-variable identifiers to expressions.