Trait SpecPred 

pub trait SpecPred<T> {
    // Required method
    spec fn apply(&self, value: T) -> bool;
}

Spec-level predicate abstraction.

Required Methods

spec fn apply(&self, value: T) -> bool

Applies the predicate to a value.

Implementations on Foreign Types

impl<T, P: SpecPred<T>> SpecPred<T> for &P

open spec fn apply(&self, value: T) -> bool

{ (*self).apply(value) }

Implementors

impl SpecPred<PrintableStringSpec> for NumericStringChars

impl<T> SpecPred<T> for PredFnSpec<T>

impl<T, Exec, Spec> SpecPred<<T as DeepView>::V> for FnPred<T, Exec, Spec>

where T: DeepView, Exec: Fn(&T) -> bool, Spec: SpecPred<T::V>,

impl<T, L: SpecPred<T>, R: SpecPred<T>> SpecPred<T> for ConstraintAnd<L, R>

impl<T, L: SpecPred<T>, R: SpecPred<T>> SpecPred<T> for ConstraintOr<L, R>

impl<T, P: SpecPred<T>> SpecPred<T> for ConstraintNot<P>

impl<T, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<Seq<T>> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<i8> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<i16> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> SpecPred<int> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<BmpStringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<Ia5StringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<PrintableStringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<TeletexStringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>