- 14 Apr, 2021 1 commit
-
-
Lennard Gäher authored
-
- 08 Dec, 2020 1 commit
-
-
Simon Spies authored
-
- 28 Nov, 2020 1 commit
-
-
Lennard Gäher authored
-
- 24 Nov, 2020 3 commits
-
-
Ralf Jung authored
-
Lennard Gäher authored
-
Lennard Gäher authored
-
- 22 Jul, 2019 1 commit
-
-
Ralf Jung authored
-
- 14 Jul, 2019 4 commits
-
-
Robbert Krebbers authored
Add `big_sepL2_app_inv_2`. See merge request iris!292
-
And shorten the proof.
-
Robbert Krebbers authored
Add `head_prim_fill_reducible`. See merge request iris!293
-
A more general implication from `head_reducible` to `reducible`.
-
- 13 Jul, 2019 7 commits
-
-
Robbert Krebbers authored
Mark projections for sigTO as NonExpansive and Proper See merge request iris!285
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
show that pair construction commutes with taking the core See merge request iris!286
-
Ralf Jung authored
-
- 12 Jul, 2019 2 commits
- 09 Jul, 2019 4 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Get rid of a superflous argument to `fresh_locs`. See merge request iris!288
-
Dan Frumin authored
-
Ralf Jung authored
-
- 07 Jul, 2019 1 commit
-
-
Ralf Jung authored
-
- 05 Jul, 2019 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 03 Jul, 2019 4 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
- 01 Jul, 2019 4 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
- 30 Jun, 2019 2 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- 29 Jun, 2019 1 commit
-
-
Ralf Jung authored
This also gets rid of [val_for_compare]-normalization; instead we introduce a [LitErased] literal that is suited for use by erasure theorems.
-
- 28 Jun, 2019 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This commit made me cry...
-