Struct ProofSkeleton 

pub struct ProofSkeleton {
    pub term: Expr,
    pub ty: Expr,
    pub holes: Vec<Name>,
}

A proof skeleton: a proof term with holes (sorry) that need to be filled.

Proof skeletons are used in structured proof construction to track what remains to be proved.

Fields

term: Expr

The proof term, which may contain sorry nodes.

ty: Expr

The type (proposition) being proved.

holes: Vec<Name>

Names of the holes that still need proofs.

Implementations

impl ProofSkeleton

pub fn new(term: Expr, ty: Expr) -> Self

Create a new proof skeleton.

pub fn is_complete(&self) -> bool

Whether the skeleton has no remaining holes.

pub fn num_holes(&self) -> usize

Number of remaining holes.

Trait Implementations

impl Clone for ProofSkeleton

fn clone(&self) -> ProofSkeleton

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofSkeleton

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

Formats the value using the given formatter.

impl Display for ProofSkeleton

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

Formats the value using the given formatter.