Struct FnPred 

pub struct FnPred<T: DeepView, Exec: Fn(&T) -> bool, Spec: SpecPred<T::V>> { /* private fields */ }

Pairs an executable predicate closure with a ghost spec predicate.

Implementations

impl<T, Exec, Spec> FnPred<T, Exec, Spec>

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

pub exec fn new(exec_fn: Exec, Ghost(spec): Ghost<Spec>) -> pred : Self

requires

forall |v: &T| #[trigger] call_requires(exec_fn, (v,)),

forall |v: &T, ok: bool| {
    #[trigger] call_ensures(exec_fn, (v,), ok) ==> ok == spec.apply(v.deep_view())
},

Trait Implementations

impl<T, Exec, Spec> Pred<T> for FnPred<T, Exec, Spec>

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

exec fn test(&self, value: &T) -> ok : bool

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>,

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