Added TCForall2_Forall2 lemma (!107) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Michael Sammler requested to merge msammler/stdpp:tcforall2_forall into master 5 years ago

All threads resolved!

This lemma existed for TCForall but not for TCForall2.

Edited 5 years ago by Robbert Krebbers

Activity

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

Resolved 5 years ago by Michael Sammler
Last reply by Michael Sammler 5 years ago

Robbert Krebbers @robbertkrebbers · 5 years ago

Owner

Thanks, LGTM modulo one nit.

Michael Sammler added 1 commit 5 years ago

added 1 commit

c0680952 - Update theories/list.v

Compare with previous version

Michael Sammler added 1 commit 5 years ago

added 1 commit

81f9b193 - added tcforall2_forall lemma

Compare with previous version

Michael Sammler resolved all threads 5 years ago

resolved all threads

Robbert Krebbers changed title from Added tcforall2_forall2 lemma to Added TCForall2_Forall2 lemma 5 years ago

changed title from Added tcforall2_forall2 lemma to Added TCForall2_Forall2 lemma

Robbert Krebbers merged 5 years ago

merged

Robbert Krebbers mentioned in commit 5 years ago

mentioned in commit 070f2235

Robbert Krebbers @robbertkrebbers · 5 years ago

Owner

Merged. Thanks!

Please register or sign in to reply