Trait creusot_contracts::std::ops::FnOnceExt

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;
}

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

type Output

Required Methods

fn precondition(self, a: Args) -> bool

logic(prophetic)

fn postcondition_once(self, a: Args, res: Self::Output) -> bool

logic(prophetic)

Implementors

impl<Args: Tuple, F: FnOnce<Args>> FnOnceExt<Args> for F

type Output = <F as FnOnce<Args>>::Output