Skip to content
scrambled
Programming Language Theory Concept

Proof by rewriting

Books JourneyProgramming Language Theory Statuslearning

  • (Proof/Reason technique, Logic) A Proof technique that transforms expressions by substituting equals for equals, using known equalities to reshape the Goal.

  • (Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) Rocq A Proof techniques in Rocq (via rewrite) that substitutes equals for equals using a known equality to transform the Goal.