pub trait FnOnceExt<Args: Tuple> {
type Output;
// Required methods
fn precondition(self, a: Args) -> bool;
fn postcondition_once(self, a: Args, res: Self::Output) -> bool;
}Expand description
FnOnceExt is an extension trait for the FnOnce trait, used for
adding a specification to closures. It should not be used directly.
Required Associated Types§
Required Methods§
Sourcefn precondition(self, a: Args) -> bool
fn precondition(self, a: Args) -> bool
(prophetic) ⚠
Sourcefn postcondition_once(self, a: Args, res: Self::Output) -> bool
fn postcondition_once(self, a: Args, res: Self::Output) -> bool
(prophetic) ⚠