Struct CvlrImplies 

pub struct CvlrImplies<A, B>(/* private fields */);

A boolean expression representing logical implication (A → B).

This expression evaluates to true when either the antecedent A is false, or when both A and B are true. When asserting or assuming, the consequent B is only processed if the antecedent A evaluates to true.

Trait Implementations

impl<A: Clone, B: Clone> Clone for CvlrImplies<A, B>

fn clone(&self) -> CvlrImplies<A, B>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<A, B> CvlrFormula for CvlrImplies<A, B>

where A: CvlrFormula, B: CvlrFormula<Context = A::Context>,

type Context = <A as CvlrFormula>::Context

fn eval(&self, ctx: &Self::Context) -> bool

Evaluates the expression in the given context.

fn assert(&self, ctx: &Self::Context)

Asserts that the expression holds in the given context.

fn assume(&self, ctx: &Self::Context)

Assumes that the expression holds in the given context.

fn eval_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) -> bool

Evaluates the expression over two states (pre-state and post-state).

fn assert_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context)

Asserts that the expression holds across two states (pre-state and post-state).

fn assume_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context)

Assumes that the expression holds across two states (pre-state and post-state).

impl<A: Copy, B: Copy> Copy for CvlrImplies<A, B>