Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

axiom_dependencies

Returns the set of all axiom constants depended upon by term.

classify_proof

Classifies a proof term into a ProofComplexity variant.

collect_axiom_deps

Collect all axiom-like constant dependencies from an expression.

count_const_occurrences

Count the number of times a given constant name appears in term.

is_closed_term

Returns true if term contains no free variables (is a closed term).

is_proof_irrelevant

Check if proof irrelevance applies between two terms of a given type.

proof_effort

Estimate the “proof effort” metric: a rough measure of how hard it was to construct the term, based on its size and classical axiom usage.

same_proof_shape

Checks whether two proof terms have structurally identical shapes, ignoring the actual constants and literals at the leaves.