- Jun 18, 2021
-
-
Robbert Krebbers authored
Rewrite cross split lemmas so they can more easily be used for forward reasoning. See merge request !283
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 17, 2021
-
-
Robbert Krebbers authored
Various setoids lemmas for maps, lists, and option See merge request iris/stdpp!281
-
Robbert Krebbers authored
Add lemmas `map_intersection_filter` and `map_difference_filter`. See merge request iris/stdpp!282
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Jun 16, 2021
-
-
Robbert Krebbers authored
Prove more equivalences for closure operators on relations. See merge request iris/stdpp!278
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 15, 2021
-
-
Robbert Krebbers authored
As part of this: turn `rtc_nsteps` and `rtc_bsteps` into `
`s. The `_list` lemmas were proposed by @jules and he provided an initial proof specific to `rtc`. -
Robbert Krebbers authored
Misc lemmas for maps See merge request iris/stdpp!280
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 11, 2021
-
-
Robbert Krebbers authored
Misc improvements to `head` and `tail` functions for lists See merge request iris/stdpp!277
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface. Closes #94 See merge request iris/stdpp!279
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 10, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Misc setoids lemmas and tweaks for maps and option See merge request iris/stdpp!276
-
Robbert Krebbers authored
-