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

logic

ensures

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

fn core_total_idemp(self)

The specification of [core_total]

logic

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

logic(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.

logic(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

logic(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

logic(open)

None

ensures

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

fn core_total(self) -> Self

logic(open)

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

ensures

self.core() == Some(result)

fn core_total_idemp(self)

logic

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

logic

ensures

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

fn core_total(self) -> Self

logic(open)

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

ensures

self.core() == Some(result)

fn core_total_idemp(self)

logic

ensures

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

ensures

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

Implementors

impl UnitRA for Int

impl UnitRA for Nat

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

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