Trait UnitRA 

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

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

Unitary RAs are RA with a neutral element.

Required Methods

fn unit() -> Self

The unit element

ensures

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

fn core_total_idemp(self)

The specification of [core_total]

ensures

self.core_total().op(self.core_total()) == Some(self.core_total())

ensures

self.core_total().op(self) == Some(self)

Provided Methods

fn incl_refl()

In unitary RAs, the inclusion relation is reflexive

(law)

ensures

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

fn core_total(self) -> Self

In unitary RAs, the core is a total function. For better automation, it is given a simpler, total definition.

(open)

self.core_is_maximal_idemp(Self::unit());
self.core().unwrap_logic()

ensures

self.core() == Some(result)

fn unit_core()

The unit is its own core

(law)

ensures

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

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

self.core() == Some(result)

fn core_total_idemp(self)

ensures

self.core_total().op(self.core_total()) == Some(self.core_total())

ensures

self.core_total().op(self) == Some(self)

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

self.core() == Some(result)

fn core_total_idemp(self)

ensures

self.core_total().op(self.core_total()) == Some(self.core_total())

ensures

self.core_total().op(self) == Some(self)

Implementors

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

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