- Jul 24, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 21, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add ∗-∗ as notation in stdpp_scope similar to -∗. See merge request iris/iris!764
-
Ralf Jung authored -
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 30, 2023
-
-
Ralf Jung authored
Add mono_nat_own_alloc_strong See merge request iris/iris!949
-
- Jun 29, 2023
-
-
Jaemin Choi authored
-
- Jun 14, 2023
-
-
Ralf Jung authored
make fractional_split truly forwards lemmas See merge request iris/iris!945
-
-
Ralf Jung authored
-
- Jun 12, 2023
- Jun 09, 2023
-
-
Robbert Krebbers authored
add test for iInv with accessor variables See merge request iris/iris!937
-
Robbert Krebbers authored
-
Ralf Jung authored
Add some missing internal validity and equivalence lemmas for dfrac, auth and agree See merge request iris/iris!942
-
Ralf Jung authored
Remove `frac_validI`, add `dfrac_valid` See merge request iris/iris!946
-
Ike Mulder authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Ralf Jung authored
-
Ike Mulder authored
-
Ralf Jung authored
-
Ike Mulder authored
-
Ike Mulder authored
Add some missing internal validity and equivalence lemmas for dfrac, auth, agree and reservation_map
-
- Jun 08, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 06, 2023
-
-
Robbert Krebbers authored
Added missing reflexivity, symmetry, transitivity lemmas on
-
-
- Jun 05, 2023
-
-
Robbert Krebbers authored
-
- Jun 04, 2023
-
-
Ralf Jung authored
Put `Φ` of `frame_fractional` first to make it easy to specify it if Coq fails to infer it. See merge request iris/iris!943
-
Robbert Krebbers authored
-
- Jun 02, 2023
-
-
Ralf Jung authored
-
