Struct ProofTerm 

pub struct ProofTerm;

Proof term utilities.

Implementations

impl ProofTerm

pub fn is_proof(term: &Expr, prop: &Expr) -> bool

Check if an expression is a proof of a proposition.

In CiC, propositions are types in Prop. A proof is a term inhabiting such a type. Without a type checker available, we use structural heuristics.

pub fn could_be_prop(ty: &Expr) -> bool

Check if a type expression could be a proposition (in Sort 0).

A type is a Prop if its universe is Sort 0.

pub fn is_sort_zero(ty: &Expr) -> bool

Check if a type is definitely Prop (Sort 0).

pub fn get_proposition(term: &Expr) -> Option<Expr>

Extract the proposition from a proof term’s type annotation.

If the term is (t : P) where P is a Prop, returns P.

pub fn is_constructive(term: &Expr) -> bool

Check if a proof uses only constructive axioms.

A proof is constructive if it doesn’t depend on:

• Classical.choice
• Classical.em (excluded middle)
• propext (propositional extensionality, though debatable)

pub fn collect_constants(term: &Expr) -> HashSet<Name>

Collect all constant names used in a term.

pub fn size(term: &Expr) -> usize

Count the size (number of nodes) of a proof term.

pub fn depth(term: &Expr) -> usize

Compute the depth of a proof term.

pub fn same_proposition_structure(p1: &Expr, p2: &Expr) -> bool

Check if two proofs are of the same proposition structure.

When proof irrelevance is enabled, this can be used to determine if two proofs should be considered equal.