Struct AggFuncAlgebra 

pub struct AggFuncAlgebra<Commutative = NotProved, Idempotent = NotProved>(/* private fields */);

Algebraic properties for an aggregation function of type (T, &mut A) -> ().

Commutativity:

let mut state = ???;
f(a, &mut state); f(b, &mut state) // produces same final state as
f(b, &mut state); f(a, &mut state)

Idempotence:

let mut state = ???;
f(a, &mut state);
let state1 = *state;
f(a, &mut state);
// state1 must be equal to state

Implementations

impl<C, I> AggFuncAlgebra<C, I>

pub fn commutative( self, _proof: impl CommutativeProof, ) -> AggFuncAlgebra<Proved, I>

Marks the function as being commutative, with the given proof mechanism.

pub fn idempotent( self, _proof: impl IdempotentProof, ) -> AggFuncAlgebra<C, Proved>

Marks the function as being idempotent, with the given proof mechanism.

Trait Implementations

impl<C, I> Property for AggFuncAlgebra<C, I>

type Root = AggFuncAlgebra

A version of this property with all the annotations removed, on which annotations will be applied.

fn make_root(_target: &mut Option<Self>) -> Self::Root

Constructs a root instance of the property with all annotations removed.