AngouriMath
InequalityEquality
Property
Summary
Rules about equalities and inequalities.
Remarks
Run by the matcher rather than by the switch —
InequalityEquality, where its sixty-five arms are
sixty-five rules: this set writes out shapes rather than orientations, so there is
nothing for a commutative pattern to collapse. What it gains instead is that the two
De Morgan folds and the two excluded-middle rules say what they need of the bindings,
which aswitch arm says in a guard beside the shape.
InequalityEquality, where its sixty-five arms are
sixty-five rules: this set writes out shapes rather than orientations, so there is
nothing for a commutative pattern to collapse. What it gains instead is that the two
De Morgan folds and the two excluded-middle rules say what they need of the bindings,
which a
Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4405 pages online