Add `min` and `max` infix notations for `positive`. (!462) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/positive_max_min into master 2 years ago

Approval is optional

Activity

Robbert Krebbers added 1 commit 2 years ago
added 1 commit

1dcd6a62 - CHANGELOG.

Compare with previous version
Robbert Krebbers @robbertkrebbers 2 years ago

Author Owner

We have these notations for all other number types, so this is an obvious omission. Going to merge.
Robbert Krebbers enabled an automatic merge when the pipeline for 1dcd6a62 succeeds 2 years ago

enabled an automatic merge when the pipeline for 1dcd6a62 succeeds
Robbert Krebbers merged 2 years ago

merged
Robbert Krebbers mentioned in commit 52a72f29 2 years ago

mentioned in commit 52a72f29

Please register or sign in to reply