Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... (!205) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/fmap_empty into master 4 years ago

Remove duplicate map_fmap_empty of fmap_empty, and rename map_fmap_empty_inv into fmap_empty_inv for consistency's sake.

Activity

Robbert Krebbers added 1 commit 4 years ago
added 1 commit

fe6a82f9 - Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename...

Compare with previous version
Robbert Krebbers added 1 commit 4 years ago
added 1 commit

46b16f58 - Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename...

Compare with previous version
Ralf Jung @jung · 4 years ago

Owner

LGTM!
Robbert Krebbers merged 4 years ago

merged
Robbert Krebbers mentioned in commit df64edb2 4 years ago

mentioned in commit df64edb2
Robbert Krebbers @robbertkrebbers · 4 years ago

Author Owner

@iris-users This is a breaking change

Please register or sign in to reply