Skip to content

Rename `_plus` into `_add`.

This fixes #472 (closed).

See also stdpp!404 (merged)

Edited by Robbert Krebbers

Merge request reports

Loading