- Aug 11, 2022
-
-
Vincent Siles authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Generalize Propers for lists / Add some missing Params See merge request iris/stdpp!407
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Aug 10, 2022
-
-
Ralf Jung authored
Create stdpp-unstable package and add bitblast library See merge request iris/stdpp!402
-
Ralf Jung authored
-
Michael Sammler authored
-
- Aug 09, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Some `filter` lemmas make use of `map_Forall`, so put `map_Forall` before `filter.
-
Robbert Krebbers authored
Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting See merge request iris/stdpp!406
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
- strengthen set_bind_subset to have the same arity - add missing Params instance to prevent slow failures in setoid rewriting - `Proper` instances can be proven before `set_bind_ext` via `set_solver`. - `set_bind_ext` is then provable by set_solver directly.
-
Robbert Krebbers authored
Add map_seqZ See merge request iris/stdpp!391
-
- Aug 08, 2022
-
-
Robbert Krebbers authored
Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None See merge request iris/stdpp!405
-
Michael Sammler authored
-
-
Michael Sammler authored
-
- Aug 03, 2022
-
-
Robbert Krebbers authored
Add lookup_union_l' See merge request iris/stdpp!395
-
Michael Sammler authored
-
- Aug 01, 2022
-
-
Robbert Krebbers authored
Add map_agree See merge request iris/stdpp!392
-
Michael Sammler authored
-
-
Michael Sammler authored
-
Robbert Krebbers authored
Flip direction of `map_disjoint_fmap`. See merge request iris/stdpp!398
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add list_subseteq_dec See merge request iris/stdpp!400
-
Michael Sammler authored
-
- Jul 31, 2022
-
-
Robbert Krebbers authored
Add lookup lemmas for partial alter and commuting lemmas for alter See merge request iris/stdpp!399
-
Robbert Krebbers authored
-