Struct Rewrite 

pub struct Rewrite<Lhs, Rhs, Via> { /* private fields */ }

Witness that type-level expression Lhs equals Rhs, justified by rule Via.

Rewrite is a zero-sized type — it carries no data, only type-level evidence that an algebraic identity has been invoked.

Example

use karpal_proof::rewrite::*;

// Create a rewrite justified by associativity
let step: Rewrite<AssocLeft, AssocRight, ByAssociativity> =
    Rewrite::witness();

// Reverse it
let _back: Rewrite<AssocRight, AssocLeft, BySymmetry<ByAssociativity>> =
    step.sym();

Implementations

impl<Lhs, Rhs, Via> Rewrite<Lhs, Rhs, Via>

pub fn witness() -> Self

where Via: Justifies<Lhs, Rhs>,

Construct a rewrite witness.

Only compiles if Via: Justifies<Lhs, Rhs>.

pub fn sym(self) -> Rewrite<Rhs, Lhs, BySymmetry<Via>>

Reverse: if Lhs = Rhs then Rhs = Lhs.

pub fn then<Rhs2, V2>( self, _next: Rewrite<Rhs, Rhs2, V2>, ) -> Rewrite<Lhs, Rhs2, ByTransitivity<Via, V2, Rhs>>

Chain: if Lhs = Mid (via self) and Mid = Rhs2 (via next), then Lhs = Rhs2.

The Rhs of the first rewrite must be the same type as the Lhs (i.e., Mid) of the second. This is enforced by sharing the type parameter Rhs/Mid.