Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app_args

Collect the arguments from an application spine.

app_head

Return the head of an application spine (strips all Apps).

count_occurrences

Count the total number of occurrences of a sub-expression in another.

mk_and

Build And a b: logical conjunction.

mk_arrow

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

mk_arrows

Build a chain of non-dependent arrow types.

mk_const

Build a named constant with no universe parameters.

mk_eq

Build Eq α a b: the propositional equality type.

mk_lam_many

Build a lambda over a list of binders, innermost last.

mk_let

Build a let-binding let x : ty := val in body.

mk_not

Build Not p = p → False.

mk_or

Build Or a b: logical disjunction.

mk_pi_many

Build a Pi type over a list of binders.

mk_refl

Build Eq.refl α a.

prop

Convenience constructor: Prop (Sort 0).

same_head

Check if two expressions share the same head constant.

subst_expr

Substitute old with new_expr everywhere it appears in expr.

type0

Convenience constructor: Type 0 (Sort 1).

type1

Convenience constructor: Type 1 (Sort 2).