Trait QuantifierVars 

pub trait QuantifierVars<'st> {
    // Required method
    fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>];
}

This trait is implemented for types and sequences which can be used as quantified variables in forall and exists.

Required Methods

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

The concrete sequence of variable declaration which should be quantified over.

Dyn Compatibility

This trait is dyn compatible.

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

Implementations on Foreign Types

impl<'st, A, B, C, D, E> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>, Const<'st, D>, Const<'st, E>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>, D: StaticSorted<'st>, E: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B, C, D> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>, Const<'st, D>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>, D: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B, C> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>)

where A: StaticSorted<'st>, B: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st> QuantifierVars<'st> for &'st [Const<'st, Dynamic<'st>>]

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st> QuantifierVars<'st> for &'st [SortedVar<'st>]

fn into_vars(self, _st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st> QuantifierVars<'st> for Vec<Const<'st, Dynamic<'st>>>

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

Implementors

impl<'st, A> QuantifierVars<'st> for Const<'st, A>

where A: StaticSorted<'st>,