relate size of map to size of its domain (!320) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/dom-size into master 3 years ago

All threads resolved!

Activity

Robbert Krebbers @robbertkrebbers started a thread on the diff 3 years ago

Resolved 3 years ago by Ralf Jung
Last reply by Ralf Jung 3 years ago

Robbert Krebbers @robbertkrebbers · 3 years ago

Owner

Seem like useful lemmas. Thanks. I left a small comment.

Ralf Jung added 1 commit 3 years ago

added 1 commit

efdc3e48 - make name more consistent

Compare with previous version

Ralf Jung resolved all threads 3 years ago

resolved all threads

Ralf Jung added 7 commits 3 years ago

added 7 commits

efdc3e48...608a079a - 4 commits from branch master
407d8414 - relate size of map to size of its domain
3303ec5e - make name more consistent
551b4882 - changelog

Compare with previous version

Toggle commit list

Ralf Jung enabled an automatic merge when the pipeline for succeeds 3 years ago

enabled an automatic merge when the pipeline for 551b4882 succeeds

Ralf Jung mentioned in commit 3 years ago

mentioned in commit 7d2c8d9a

Ralf Jung merged 3 years ago

merged

Please register or sign in to reply