- 02 Apr, 2020 3 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored -
Robbert Krebbers authored
-
- 01 Apr, 2020 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 20 Mar, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 16 Mar, 2020 1 commit
-
-
Ralf Jung authored
-
- 10 Mar, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 25 Feb, 2020 2 commits
-
-
Ralf Jung authored
-
Add array_copy_to (copy in-place to destination array) and array_clone (copy to a freshly allocated array). The heap_lang spec and proof for array_copy_to are inspired by https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v. Fixes #293.
-
- 23 Feb, 2020 1 commit
-
-
Tej Chajed authored
-
- 18 Feb, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 14 Feb, 2020 3 commits
- 02 Feb, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 01 Feb, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 16 Jan, 2020 1 commit
-
-
Michael Sammler authored
-
- 13 Jan, 2020 1 commit
-
-
Robbert Krebbers authored
-
- 02 Dec, 2019 1 commit
-
-
Ralf Jung authored
-
- 22 Nov, 2019 2 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- 21 Nov, 2019 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 06 Nov, 2019 1 commit
-
-
- 05 Nov, 2019 1 commit
-
-
- 01 Nov, 2019 2 commits
- 19 Sep, 2019 1 commit
-
-
Robbert Krebbers authored
-
- 11 Sep, 2019 1 commit
-
-
Robbert Krebbers authored
-
- 29 Aug, 2019 2 commits
- 28 Aug, 2019 4 commits
- 24 Aug, 2019 1 commit
-
-
Robbert Krebbers authored
-
- 13 Aug, 2019 3 commits
-
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
Turn all `f_op` lemmas to have shape `f (x ⋅ y) = f x ⋅ f y`, following the plan in iris/iris!295 (comment 39151), plus `cmra_morphism_op`.
-
