Struct Proven 

pub struct Proven<P, T> { /* private fields */ }

A value of type T accompanied by a compile-time witness that property P holds for T.

Construction is deliberately restricted: safe constructors require the relevant trait bound (e.g., from_semigroup requires T: Semigroup). The trait implementation is the proof.

For properties verified externally (proptest, SMT solver, inspection), use the unsafe Proven::axiom constructor.

Implementations

impl<P, T> Proven<P, T>

pub unsafe fn axiom(value: T) -> Proven<P, T>

Create a witness without checking.

Safety

Caller asserts that property P genuinely holds for type T.

pub fn value(&self) -> &T

Access the inner value by reference.

pub fn into_inner(self) -> T

Unwrap the witness, discarding the proof.

pub fn derive<Q>(self) -> Proven<Q, T>

where P: Implies<Q>,

If property P implies property Q, derive a new witness.

pub fn and<Q>(self, _other: Proven<Q, T>) -> Proven<And<P, Q>, T>

Combine two independent proofs into a conjunction.

impl<P, Q, T> Proven<And<P, Q>, T>

pub fn derive_second(self) -> Proven<Q, T>

Extract the second component from a conjunction proof.

(The first component is available via .derive() since And<P, Q>: Implies<P>.)

impl<T> Proven<IsAssociative, T>

where T: Semigroup,

pub fn from_semigroup(value: T) -> Proven<IsAssociative, T>

Witness associativity from a Semigroup implementation.

impl<T> Proven<IsMonoid, T>

where T: Monoid,

pub fn from_monoid(value: T) -> Proven<IsMonoid, T>

Witness monoid laws from a Monoid implementation.

impl<T> Proven<IsGroup, T>

where T: Group,

pub fn from_group(value: T) -> Proven<IsGroup, T>

Witness group laws from a Group implementation.

impl<T> Proven<IsAbelianGroup, T>

where T: AbelianGroup,

pub fn from_abelian(value: T) -> Proven<IsAbelianGroup, T>

Witness abelian group from an AbelianGroup implementation.

impl<T> Proven<IsSemiring, T>

where T: Semiring,

pub fn from_semiring(value: T) -> Proven<IsSemiring, T>

impl<T> Proven<IsRing, T>

where T: Ring,

pub fn from_ring(value: T) -> Proven<IsRing, T>

impl<T> Proven<IsField, T>

where T: Field,

pub fn from_field(value: T) -> Proven<IsField, T>

impl<T> Proven<IsLattice, T>

where T: Lattice,

pub fn from_lattice(value: T) -> Proven<IsLattice, T>

impl<T> Proven<IsBoundedLattice, T>

where T: BoundedLattice,

pub fn from_bounded_lattice(value: T) -> Proven<IsBoundedLattice, T>

Trait Implementations

impl<P, T> AbelianGroup for Proven<P, T>

where T: AbelianGroup,

impl<P, T> BoundedLattice for Proven<P, T>

where T: BoundedLattice,

fn top() -> Proven<P, T>

fn bottom() -> Proven<P, T>

impl<P, T> Clone for Proven<P, T>

where T: Clone,

fn clone(&self) -> Proven<P, T>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<P, T> Copy for Proven<P, T>

where T: Copy,

impl<P, T> Debug for Proven<P, T>

where T: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<P, T> Eq for Proven<P, T>

where T: Eq,

impl<P, T> Field for Proven<P, T>

where T: Field,

fn reciprocal(self) -> Proven<P, T>

fn div(self, other: Self) -> Self

where Self: Sized,

impl<P, T> Group for Proven<P, T>

where T: Group,

fn invert(self) -> Proven<P, T>

fn combine_inverse(self, other: Self) -> Self

where Self: Sized,

impl<P, T> Hash for Proven<P, T>

where T: Hash,

fn hash<H>(&self, state: &mut H)

where H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<P, T> Lattice for Proven<P, T>

where T: Lattice,

fn meet(self, other: Proven<P, T>) -> Proven<P, T>

fn join(self, other: Proven<P, T>) -> Proven<P, T>

impl<P, R, T> Module<R> for Proven<P, T>

where R: Ring, T: Module<R>,

fn scale(self, scalar: R) -> Proven<P, T>

impl<P, T> Monoid for Proven<P, T>

where T: Monoid,

fn empty() -> Proven<P, T>

impl<P, T> Ord for Proven<P, T>

where T: Ord,

fn cmp(&self, other: &Proven<P, T>) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl<P, T> PartialEq for Proven<P, T>

where T: PartialEq,

fn eq(&self, other: &Proven<P, T>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<P, T> PartialOrd for Proven<P, T>

where T: PartialOrd,

fn partial_cmp(&self, other: &Proven<P, T>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<P, T> Ring for Proven<P, T>

where T: Ring,

fn negate(self) -> Proven<P, T>

fn sub(self, other: Self) -> Self

where Self: Sized,

impl<P, T> Semigroup for Proven<P, T>

where T: Semigroup,

fn combine(self, other: Proven<P, T>) -> Proven<P, T>

impl<P, T> Semiring for Proven<P, T>

where T: Semiring,

fn add(self, other: Proven<P, T>) -> Proven<P, T>

fn mul(self, other: Proven<P, T>) -> Proven<P, T>

fn zero() -> Proven<P, T>

fn one() -> Proven<P, T>

impl<P, F, T> VectorSpace<F> for Proven<P, T>

where F: Field, T: VectorSpace<F>,