Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app

Shorthand: create an application.

bvar

Shorthand: create a bound variable.

collect_consts

Collect all constant names referenced in an expression.

collect_fvars

Collect all free variables in an expression.

count_lambdas

Count the number of leading lambdas.

count_pis

Count the number of leading Pi binders.

decompose_lam

Decompose a Lam expression into (binder_info, domain, body).

decompose_let

Decompose a Let expression into (type, value, body).

decompose_pi

Decompose a Pi expression into (binder_info, domain, codomain).

decompose_proj

Decompose a Proj expression into (struct_name, field_index, value).

expr_weight

Compute the “weight” of an expression (rough size metric).

for_each_expr

Traverse every sub-expression, calling f on each.

get_app_args

Extract all arguments from a chain of applications.

get_app_fn

Extract the function head from a chain of applications.

get_app_fn_args

Decompose an expression into its head function and arguments.

get_app_num_args

Get the number of arguments in an application chain.

get_bvar_idx

Extract the BVar index from a BVar expression.

get_const_levels

Extract the universe levels from a Const expression.

get_const_name

Extract the name from a Const expression.

get_fvar_id

Extract the FVarId from an FVar expression.

get_nth_arg

Get the n-th argument in an application chain (0-indexed).

get_sort_level

Extract the level from a Sort expression.

has_any_fvar

Check if an expression contains any free variables.

has_fvar

Check if an expression contains a specific free variable.

has_level_mvar

Check if an expression has universe level metavariables.

has_level_param

Check if an expression contains any level parameters.

has_loose_bvar

Check if an expression has a specific loose bound variable at level.

has_loose_bvar_ge

Check if an expression has a loose bound variable with index >= depth.

has_loose_bvars

Check if an expression has any loose bound variables.

is_app

Check if the expression is an App.

is_app_of

Check if the head of an application is a constant with a specific name.

is_app_of_fvar

Check if e is an application of FVar id.

is_bvar

Check if the expression is a BVar.

is_const

Check if the expression is a Const.

is_fvar

Check if the expression is an FVar.

is_lambda

Check if the expression is a lambda abstraction.

is_let

Check if the expression is a Let.

is_literal

Check if the expression is a Literal.

is_pi

Check if the expression is a Pi type.

is_proj

Check if the expression is a Proj.

is_prop

Check if the expression is Sort(Level::Zero) (i.e. Prop).

is_simple

Check if an expression is “simple” (atomic: no subexpressions).

is_sort

Check if the expression is a Sort.

is_type0

Check if the expression is Sort(Level::Succ(Level::Zero)) (i.e. Type 0).

lam

Shorthand: create a lambda.

level_has_mvar

Check if a level has metavariables.

lift_loose_bvars

Lift (shift) loose bound variables by n.

mk_app

Construct an application from a function and a list of arguments.

mk_app_range

Construct an application from a function and a range of arguments.

mk_arrow

Build a non-dependent arrow type: a → b.

mk_lam_n

Build a nested Lam abstraction from a list of binders and a body.

mk_pi_n

Build a nested Pi type from a list of binders and a return type.

mk_prop

Build Sort 0 (Prop).

mk_type

Build Sort (u + 1) (Type u).

mk_type0

Build Sort 1 (Type 0).

occurs_const

Check if a constant name occurs anywhere in an expression.

pi

Shorthand: create a pi type.

prop

Shorthand: Prop = Sort 0.

replace_expr

Replace sub-expressions using a callback.

sort

Shorthand: Sort(Level::zero()).

strip_lambdas

Get the body after stripping n leading lambdas.

strip_pis

Get the body after stripping n leading Pis.

type0

Shorthand: Type 0 = Sort 1.

var

Shorthand: create a constant expression.