treat Forall2 constructors like we treat Forall constructors (!318) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/Forall2 into master 3 years ago

All threads resolved!

In particular, have a lemma Forall2_cons that is an ↔.

For consistency, rename Forall2_cons_inv to Forall2_cons_1 (matching Forall_cons_1).

Someone should probably do the same for Forall3...

Edited 3 years ago by Ralf Jung

Activity

Ralf Jung changed the description 3 years ago

changed the description
Ralf Jung mentioned in issue simuliris#12 3 years ago

mentioned in issue simuliris#12
Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

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

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers 3 years ago

Owner

Modulo comment LGTM.

Ralf Jung added 1 commit 3 years ago

added 1 commit

b4f29dc0 - tweak comments; changelog

Compare with previous version

Ralf Jung resolved all threads 3 years ago

resolved all threads

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Ralf Jung

Ralf Jung resolved all threads 3 years ago

resolved all threads

Ralf Jung added 1 commit 3 years ago

added 1 commit

68f87208 - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

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

enabled an automatic merge when the pipeline for 68f87208 succeeds

Ralf Jung mentioned in commit 3 years ago

mentioned in commit a3841e4d

Ralf Jung merged 3 years ago

merged

Please register or sign in to reply