Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

apply_k

Apply the K combinator: K x y = x.

beta_applicative_order

Applicative-order beta reduction.

beta_equivalent

Check if two expressions are beta-equivalent.

beta_head_normalize

Head beta normalization: reduce only the head of an application spine.

beta_normal_order

Normal-order beta reduction.

beta_normalize

Perform beta reduction to normal form.

beta_normalize_fueled

Perform fueled beta normalization.

beta_normalize_with_stats

Beta reduce with statistics collection.

beta_step

Perform one step of beta reduction.

beta_step_with_flag

Perform one step of beta reduction at the outermost position.

beta_under_binder

Beta reduce under a specific variable binding.

beta_whnf

Reduce an expression to weak head normal form.

collect_app_spine

Collect the application spine of an expression.

count_redexes

Count the number of redexes at the outermost position.

count_reduction_steps

Count the number of beta reduction steps to normalize an expression.

estimate_reduction_depth

Estimate how many steps are needed to normalize an expression.

eta_expand

Eta-expand an expression of a known function type.

eta_reduce

Eta-reduce lambda x. f x to f when x is not free in f.

has_let

Check if an expression contains any let-bindings.

is_beta_normal

Check if an expression is in beta normal form.

is_eta_reducible

Check if an expression is eta-reducible.

is_whnf

Check if an expression is in weak head normal form.

mk_beta_redex

Create a beta redex (lambda application that can be reduced).

mk_compose

Compose two functions: lambda x : dom. f (g x).

mk_const_fn

Create a constant function: lambda _ : dom. val.

mk_i_combinator

Create an I combinator: lambda x. x.

mk_identity

Create an identity function for a given type: lambda x : ty. x.

mk_k_combinator

Create a K combinator: lambda x. lambda y. x.

mk_multi_beta_redex

Create a multi-argument beta redex.

reduce_app_spine

Reduce an application spine.

reduce_lets

Reduce all let-bindings by substitution.