Struct HypContext 

pub struct HypContext { /* private fields */ }

A context that supports multiple named local hypotheses (proof state).

Implementations

impl HypContext

pub fn new() -> Self

Create an empty hypothesis context.

pub fn add_hyp(&mut self, name: Name, ty: Expr) -> FVarId

Add a hypothesis with the given name and type.

pub fn find_hyp(&self, name: &Name) -> Option<FVarId>

Look up a hypothesis by name (searches from innermost).

pub fn hyp_type(&self, fvar: FVarId) -> Option<&Expr>

Get the type of a hypothesis.

pub fn num_hyps(&self) -> usize

Number of hypotheses.

pub fn hyp_names(&self) -> Vec<&Name>

All hypothesis names.

pub fn remove_last_hyp(&mut self)

Remove the last added hypothesis.

pub fn clear(&mut self)

Clear all hypotheses.

Trait Implementations

impl Clone for HypContext

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for HypContext

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

Formats the value using the given formatter.

impl Default for HypContext

fn default() -> Self

Returns the “default value” for a type.