Trait SpecMap 

pub trait SpecMap {
    type Input;
    type Output;

    // Required method
    spec fn spec_map(&self, i: Self::Input) -> Self::Output;
}

Required Associated Types

type Input

type Output

Required Methods

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

Implementations on Foreign Types

impl<I, O> SpecMap for FnSpec<(I,), O>

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

{ (self)(i) }

type Input = I

type Output = O

Implementors

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

type Input = <I as DeepView>::V

type Output = <O as DeepView>::V