Trait UnitRA 

pub trait UnitRA: RA {
    // Required methods
    fn unit() -> Self;
    fn core_is_total(self);

    // Provided methods
    fn incl_refl() { ... }
    fn unit_core() { ... }
    fn core_total(self) -> Self { ... }
}

Required Methods

fn unit() -> Self

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_is_total(self)

ensures

self.core() == Some(self.core_total())

Provided Methods

fn incl_refl()

(law, sealed)

ensures

forall<x: Self> x.incl(x)

fn unit_core()

(law, sealed)

ensures

Self::unit().core_total() == Self::unit()

fn core_total(self) -> Self

(open)

let _ = self.core_is_maximal_idemp(Self::unit());
self.core().unwrap_logic()

ensures

result.op(result) == Some(result)

ensures

result.op(self) == Some(self)

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<T: RA> UnitRA for Option<T>

fn unit() -> Self

(open)

None

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_total(self) -> Self

(open)

match self {
    None => None,
    Some(x) => x.core(),
}

ensures

result.op(result) == Some(result)

ensures

result.op(self) == Some(self)

fn core_is_total(self)

ensures

self.core() == Some(self.core_total())

impl<T: UnitRA, U: UnitRA> UnitRA for (T, U)

fn unit() -> Self

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_total(self) -> Self

(open)

(self.0.core_total(), self.1.core_total())

ensures

result.op(result) == Some(result)

ensures

result.op(self) == Some(self)

fn core_is_total(self)

ensures

self.core() == Some(self.core_total())

Implementors

impl<K, V: RA> UnitRA for FMap<K, V>

impl<R: ViewRel> UnitRA for View<R>