Skip to main content

CommutativeProof

Trait CommutativeProof 

Source
pub trait CommutativeProof: Sealed {
    // Required method
    fn register_proof(&self, expr: &Expr);
}
Expand description

A trait for proof mechanisms that can validate commutativity.

Required Methods§

Source

fn register_proof(&self, expr: &Expr)

Registers the expression with the proof mechanism.

This should not perform any blocking analysis; it is only intended to record the expression for later processing.

Implementors§