Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

alpha_eq

Check if two expressions are alpha-equivalent (structurally equal).

contains_bvar

Check if an expression contains the given de Bruijn variable.

decompose_app

Collect the arguments of a spine application f a1 a2 … an.

eta_reduce

Remove eta-redexes: (fun x => f x) → f (when x not free in f).

eval_nat

Evaluate a closed Nat arithmetic expression to a literal, if possible.

expr_depth

Return the depth (longest path to leaf) of an expression.

expr_size

Return the AST size (number of nodes) of an expression.

fold_nat_constants

Fold constant Nat arithmetic in an expression (recursive).

free_vars

Collect all FVarIds appearing in expr.

is_app_of

Check if expr is headed by constant head_name.

is_closed

Return true if expr contains no free variables.

is_false_expr

Check if expr is the constant False.

is_nat_lit

Check whether expr is a Nat literal with value n.

is_prop

Check if expr is Prop (Sort 0).

is_succ

Check whether expr is Nat.succ _.

is_true

Check if expr is the constant True.

is_zero

Check whether expr is Nat.zero or the literal 0.

mk_app

Build an application spine from a head and argument list.

normalize

Normalize an expression (reduce to normal form).

rewrite_all

Apply a rewrite rule exhaustively until no more rewrites are possible.

rewrite_once

Apply a single rewrite rule lhs = rhs throughout expr.

simp_congruence

Apply simplify to all sub-expressions one level deep.

simp_with_trace

Apply a SimpLemmaSet and record which lemmas were used.

simplify

Simplify an expression using basic rewrite rules.

simplify_bounded

Simplify to a maximum depth (prevents looping on large terms).

succ_of

Extract the predecessor from a Nat.succ n expression.