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()