Add little endian encoding of Z (!254) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Michael Sammler requested to merge msammler/little_endian into master 4 years ago

Approval is optional

Activity

Michael Sammler mentioned in merge request !250 (closed) 4 years ago

mentioned in merge request !250 (closed)
Michael Sammler added 1 commit 4 years ago
added 1 commit

04f49ac3 - Add little endian encoding of Z

Compare with previous version
Ralf Jung @jung started a thread on an old version of the diff 4 years ago

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

Ralf Jung @jung started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Michael Sammler

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

Resolved 4 years ago by Michael Sammler

Michael Sammler added 1 commit 4 years ago

added 1 commit

fdff3f73 - Add little endian encoding of Z

Compare with previous version

Michael Sammler resolved all threads 4 years ago

resolved all threads

Michael Sammler added 4 commits 4 years ago

added 4 commits

fdff3f73...3652e6e8 - 3 commits from branch master
480d7754 - Add little endian encoding of Z

Compare with previous version

Robbert Krebbers added 1 commit 4 years ago

added 1 commit

8552be36 - Tweak proofs.

Compare with previous version

Robbert Krebbers @robbertkrebbers 4 years ago

Owner

I tweaked the proofs a bit. It turned out that all uses of nia can be replaced by lia.

Robbert Krebbers added 1 commit 4 years ago

added 1 commit

88cd2340 - Fix comment. Thanks @mpu.

Compare with previous version

Robbert Krebbers @robbertkrebbers 4 years ago

Owner

@jung Any opinions?

Robbert Krebbers added 3 commits 4 years ago

added 3 commits

54252fbc - 1 commit from branch master
955eba16 - Add little endian encoding of Z
4afcc624 - Tweak proofs.

Compare with previous version

Ralf Jung @jung started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Michael Sammler @msammler 4 years ago

Author Owner

Resolved 4 years ago by Michael Sammler

@robbertkrebbers I've had to replace some of the uses of lia by nia as the proofs otherwise do not work on Coq 8.10.2.
Last reply by Michael Sammler 4 years ago

Michael Sammler added 1 commit 4 years ago

added 1 commit

6b108c6a - tweak comment and fix proofs

Compare with previous version

Ralf Jung @jung started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Michael Sammler added 1 commit 4 years ago

added 1 commit

2b8ad872 - tweak comment

Compare with previous version

Ralf Jung @jung started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Michael Sammler

Michael Sammler added 1 commit 4 years ago

added 1 commit

47a51f7a - fix implicit types

Compare with previous version

Please register or sign in to reply