Type Alias FnSpecMapper 

pub type FnSpecMapper<In, Out> = (FnSpec<(In,), Out>, FnSpec<(Out,), In>);

Trait Implementations

impl<In, Out> SpecMapper for FnSpecMapper<In, Out>

open spec fn spec_map(&self, i: Self::In) -> Self::Out

{ (self.0)(i) }

open spec fn spec_map_rev(&self, o: Self::Out) -> Self::In

{ (self.1)(o) }

type In = In

The input type.

type Out = Out

The output type.

fn wf_in(&self, i: Self::In) -> bool

fn wf_out(&self, o: Self::Out) -> bool