Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation

Marcus Rossel, Rudi Schneider, Thomas Koehler, Michel Steuwer, Andrés Goens
January 2026
PDF DOI
Type
Journal article
Publication
Proc. ACM Program. Lang.