Macro creusot_contracts::ord_laws_impl

macro_rules! ord_laws_impl {
    () => { ... };
}

A macro to easily implements the various #[law]s of OrdLogic.

Usage

Simply use this macro in the trait impl:

use ::std::cmp::Ordering;
struct MyInt(Int);

impl OrdLogic for MyInt {
    #[logic] #[open(self)]
    fn cmp_log(self, other: Self) -> Ordering { todo!() }
    #[logic] #[open(self)]
    fn le_log(self, other: Self) -> Ordering { todo!() }
    #[logic] #[open(self)]
    fn lt_log(self, other: Self) -> Ordering { todo!() }
    #[logic] #[open(self)]
    fn ge_log(self, other: Self) -> Ordering { todo!() }
    #[logic] #[open(self)]
    fn gt_log(self, other: Self) -> Ordering { todo!() }

    ord_laws_impl! {}
}