Add natural numbers with min RA
Related to #324 (closed) this MR adds a resource algebra with natural numbers as the carrier and min as the operation.
The MR names the RA
min_nat and uses the boxed approach suggested by @robbertkrebbers in #324 (comment 52393). I did make a small change by defining the record field with a
:> such that instances of the RA coerce to
nats. I'm not sure if there are any downsides to that as well, but it seemed convenient.
If this is how we decide that the
min_nat RA should be implemented then the current
mnat RA should be changed accordingly: renamed to
max_nat, get boxed, and these breaking changes should be documented in the changelog.
Closes #324 (closed).