Macro manual_proof 

macro_rules! manual_proof {
    ($(#[doc = $doc:expr])+) => { ... };
}

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

use hydro_lang::prelude::*;

stream.fold(
    q!(|| 0),
    q!(
        |acc, x| *acc += x,
        commutative = manual_proof!(/** integer addition is commutative */)
    )
)