Macro partial_ord_laws_impl 

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

A macro to easily implements the various #[logic(law)]s of PartialOrdLogic.

Usage

Simply use this macro in the trait impl:

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

impl PartialOrdLogic for MyInt {
    #[logic(open)]
    fn lt_log(self, other: Self) -> bool { todo!() }

    partial_ord_laws_impl! {}
}

impl OrdLogic for MyInt {
    #[logic(law)]
    #[ensures(self < other || self == other || other < self)]
    fn lt_log_total(self, other: Self) {}
}

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 PartialOrdLogic for MyInt {
    #[logic(open)]
    fn lt_log(self, other: Self) -> bool { todo!() }

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