Macro ord_laws_impl 

macro_rules! ord_laws_impl {
    ( $($lemma:stmt)* ) => { ... };
}

A macro to easily implements the various #[logic(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]
    fn cmp_log(self, other: Self) -> Ordering { todo!() }
    #[logic]
    fn le_log(self, other: Self) -> bool { todo!() }
    #[logic]
    fn lt_log(self, other: Self) -> bool { todo!() }
    #[logic]
    fn ge_log(self, other: Self) -> bool { todo!() }
    #[logic]
    fn gt_log(self, other: Self) -> bool { todo!() }

    ord_laws_impl! {}
}

Additionally, you can define instructions that will be injected in every generated law’s body. This can be useful to apply a lemma to every law:

#[opaque]
pub struct MyInt(());

impl View for MyInt {
    type ViewTy = Int;
    #[logic(opaque)] fn view(self) -> Int { dead }
}

impl MyInt {
    #[trusted]
    #[logic]
    #[ensures(self@ == other@ ==> self == other)]
    fn view_inj(self, other: Self) {}
}

impl OrdLogic for MyInt {
    #[logic(open)]
    fn cmp_log(self, other: Self) -> Ordering { pearlite! { self@.cmp_log(other@) } }
    // ...

    ord_laws_impl! { let _ = MyInt::view_inj; }
}