Trait vstd::pcm::PCM

source · 
pub trait PCM: Sized {
    // Required methods
    fn valid(self) -> bool;
    fn op(self, other: Self) -> Self;
    fn unit() -> Self;
    fn closed_under_incl(a: Self, b: Self);
    fn commutative(a: Self, b: Self);
    fn associative(a: Self, b: Self, c: Self);
    fn op_unit(a: Self);
    fn unit_valid();
}
Expand description

See Resource for more information.

Required Methods§

source

spec fn valid(self) -> bool

source

spec fn op(self, other: Self) -> Self

source

spec fn unit() -> Self

source

proof fn closed_under_incl(a: Self, b: Self)

source

proof fn commutative(a: Self, b: Self)

source

proof fn associative(a: Self, b: Self, c: Self)

source

proof fn op_unit(a: Self)

source

proof fn unit_valid()

Object Safety§

This trait is not object safe.

Implementors§