Trait FnExt 

pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
    // Required methods
    fn postcondition(self, _: Args, _: Self::Output) -> bool;
    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output);
    fn fn_once(self, args: Args, res: Self::Output);
    fn fn_hist_inv(self, res_state: Self);
}

FnExt is an extension trait for the Fn trait, used for adding a specification to closures. It should not be used directly.

Required Methods

fn postcondition(self, _: Args, _: Self::Output) -> bool

(prophetic)

fn fn_mut(self, args: Args, res_state: Self, res: Self::Output)

(law)

ensures

self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state)

fn fn_once(self, args: Args, res: Self::Output)

(law)

ensures

self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self))

fn fn_hist_inv(self, res_state: Self)

(law)

ensures

self.hist_inv(res_state) == (self == res_state)

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<Args: Tuple, F: ?Sized + Fn<Args>> FnExt<Args> for F

Available on crate feature nightly only.