pub trait PCM: Sized {
// Required methods
spec fn valid(self) -> bool;
spec fn op(self, other: Self) -> Self;
spec fn unit() -> Self;
proof fn closed_under_incl(a: Self, b: Self);
proof fn commutative(a: Self, b: Self);
proof fn associative(a: Self, b: Self, c: Self);
proof fn op_unit(a: Self);
proof fn unit_valid();
}
Expand description
See Resource
for more information.
Required Methods§
Sourceproof fn closed_under_incl(a: Self, b: Self)
proof fn closed_under_incl(a: Self, b: Self)
requires
Self::op(a, b).valid(),
ensuresa.valid(),
Sourceproof fn commutative(a: Self, b: Self)
proof fn commutative(a: Self, b: Self)
ensures
Self::op(a, b) == Self::op(b, a),
Sourceproof fn associative(a: Self, b: Self, c: Self)
proof fn associative(a: Self, b: Self, c: Self)
ensures
Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
Sourceproof fn unit_valid()
proof fn unit_valid()
ensures
Self::valid(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.