Struct ProofAnalysis 

pub struct ProofAnalysis {
    pub size: usize,
    pub depth: usize,
    pub lambda_count: usize,
    pub app_count: usize,
    pub let_count: usize,
    pub fvar_count: usize,
    pub bvar_count: usize,
    pub uses_classical: bool,
    pub constants: HashSet<Name>,
}

A record describing the structure of a proof term for analysis.

Fields

size: usize

Total AST node count.

depth: usize

Maximum nesting depth.

lambda_count: usize

Number of lambda abstractions.

app_count: usize

Number of applications.

let_count: usize

Number of let-bindings.

fvar_count: usize

Number of free variables referenced.

bvar_count: usize

Number of bound variable references.

uses_classical: bool

Whether the term contains any classical axiom.

constants: HashSet<Name>

Names of all constants referenced.

Implementations

impl ProofAnalysis

pub fn analyse(term: &Expr) -> Self

Analyse a proof term and return a ProofAnalysis.

Trait Implementations

impl Clone for ProofAnalysis

fn clone(&self) -> ProofAnalysis

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofAnalysis

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.