Skip to main content

__manual_proof__

Macro __manual_proof__ 

Source
macro_rules! __manual_proof__ {
    ($(#[doc = $doc:expr])+) => { ... };
}
Expand description

Fulfills a proof parameter by declaring a human-written justification for why the algebraic property (e.g. commutativity, idempotence) holds.

The argument must be a doc comment explaining why the property is satisfied.

ยงExamples

// stream: [1, 2, 3] (unordered)
stream
    .fold(
        q!(|| 0),
        q!(
            |acc, x| *acc += x,
            commutative = manual_proof!(/** integer addition is commutative */)
        ),
    )
    .into_stream()