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".

Implementations on Foreign Types

impl<T1: UnitRA, T2: UnitRA, T3: UnitRA, T4: UnitRA> UnitRA for (T1, T2, T3, T4)

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.$n.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)

impl<T1: UnitRA, T2: UnitRA, T3: UnitRA> UnitRA for (T1, T2, T3)

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.$n.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)

impl<T1: UnitRA, T2: UnitRA> UnitRA for (T1, T2)

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.$n.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)

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)

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>