search

andrewchawk / casanova-fly

Casanova Fly is a formally-verified computer algebra system.
The Unlicense
0 stars 0 forks source link

Datatype-Based Algebraic Equality Type #5

Closed andrewchawk closed 2 months ago

andrewchawk commented 2 months ago

This change converts AlgebraicEquality into a thing which is primarily data-based, as opposed to being _⊎_-based. This change facilitates stuff like the addition of new equality rules.

andrewchawk commented 2 months ago

I do think that some of the current documentation is undesirably repetitive. However, I suppose that having some undesirably repetitive documentation is preferable to having no documentation. :-)

Aside from further abstraction, which is being planned, I am uncertain of a real method of reducing this repetition. Anyway, to keep this merge simple, I suppose that I will improve the documentation or do further abstraction at some unspecified later date.