Trait ProofContext 

pub trait ProofContext {
    // Required methods
    fn lookup(&self, name: &str) -> Result<Option<ProofName>>;
    fn ctors(&self, data: &str) -> Vec<Ctor>;
}

The checker’s view of the program, as a proof sees it.

Required Methods

fn lookup(&self, name: &str) -> Result<Option<ProofName>>

Resolves a (dotted) name from the theorem’s module.

Errors

When the name climbs above the crate root.

fn ctors(&self, data: &str) -> Vec<Ctor>

The constructors of a data type.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors