Struct FnMap 

pub struct FnMap<I: DeepView, O: DeepView, Exec: Fn(I) -> O, Spec: SpecMap<Input = I::V, Output = O::V>> { /* private fields */ }

Pairs an executable predicate closure with a ghost spec predicate.

Implementations

impl<I: DeepView, O: DeepView, Exec: Fn(I) -> O, Spec: SpecMap<Input = I::V, Output = O::V>> FnMap<I, O, Exec, Spec>

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

requires

forall |i: I| #[trigger] call_requires(exec_fn, (i,)),

forall |i: I, o: O| {
    #[trigger] call_ensures(exec_fn, (i,), o)
        ==> o.deep_view() == spec_fn.spec_map(i.deep_view())
},

Trait Implementations

impl<I, O, Exec, Spec> Map<I> for FnMap<I, O, Exec, Spec>

where I: DeepView, O: DeepView, Exec: Fn(I) -> O, Spec: SpecMap<Input = I::V, Output = O::V>,

exec fn map(&self, i: I) -> o : Self::O

type O = O

impl<I, O, Exec, Spec> SpecMap for FnMap<I, O, Exec, Spec>

where I: DeepView, O: DeepView, Exec: Fn(I) -> O, Spec: SpecMap<Input = I::V, Output = O::V>,

closed spec fn spec_map(&self, i: Self::Input) -> Self::Output

type Input = <I as DeepView>::V

type Output = <O as DeepView>::V